Resumen:Presentamos **Lean4PHYS**, un marco de razonamiento integral para problemas de física de nivel universitario en Lean4. **Lean4PHYS** incluye *LeanPhysBench*, un punto de referencia de nivel universitario para el razonamiento de física formal en Lean4, que contiene 200 declaraciones hechas a mano y revisadas por pares derivadas de libros de texto universitarios y problemas de competencia de física. Para establecer una base sólida para el razonamiento formal en física, también presentamos *PhysLib*, un repositorio impulsado por la comunidad que contiene sistemas de unidades fundamentales y teoremas esenciales para el razonamiento en física formal. Con base en el punto de referencia y el repositorio Lean4 que compusimos en **Lean4PHYS**, informamos los resultados de referencia utilizando los principales probadores expertos de Math Lean4 y modelos de código cerrado de última generación, con el mejor rendimiento de DeepSeek-Prover-V2-7B logrando solo el 16 % y Claude-Sonnet-4 logrando el 35 %. También realizamos un análisis detallado que muestra que nuestro *PhysLib* puede lograr una mejora promedio del 11,75% en el rendimiento del modelo. Esto demuestra la naturaleza desafiante de nuestro *LeanPhysBench* y la efectividad de *PhysLib*. Hasta donde sabemos, este es el primer estudio que proporciona un punto de referencia de física en Lean4.
Publicado originalmente en export.arxiv.org el 30 de octubre de 2025.
Ver fuente original
