Putnam, el concurso de matemáticas para estudiantes universitarios más difícil del mundo, finalizó ayer a las 4 p. m. (hora del Pacífico). A las 3:58 p. m., AxiomProver @axiommathai resolvió de forma autónoma 8/12 de Putnam2025 en Lean, un lenguaje 100 % verificable. El año pasado, nuestra puntuación habría sido la número 4 de ~4000 y un Putnam Fellow (entre los 10 mejores en los últimos años).
El examen William Lowell Putnam es la competición universitaria más prestigiosa del mundo. La puntuación media suele ser 0. Axiom es una startup de Palo Alto con 4 meses de vida. Estamos construyendo el punto de partida para el razonamiento: un matemático de IA. Lean es un lenguaje 100% verificable por máquinas.
Este es nuestro primer paso. Hace cuatro meses, compramos sillas de camping y mesas de plástico en una venta de garaje. Había pizarras blancas en las paredes. Todos estaban encantados con nuestro primer sofá. Ahora echamos raíces al otro lado del Atlántico. ¡Un equipo con increíbles conocimientos de matemáticas e ingeniería se une!
A las personas detrás de nuestro sistema AxiomProver les encantan las matemáticas, los lenguajes de programación y la IA: los tres pilares. Debaten sobre si una formalización es natural. Se entusiasman cuando se ejecuta una prueba gracias a las técnicas del compilador. Este trabajo es técnico, pero también profundamente humano.
Nos apoyamos en los hombros de gigantes: @leanprover, la comunidad Mathlib y los investigadores académicos e industriales. Gracias, estamos desarrollando herramientas para servir a la comunidad a través de futuras versiones. Saludamos a los participantes de Putnam y celebraremos sus logros muy pronto.
¡@axiommathai agradecería tus retuits!