7 papers
Does My Embedding Reflect That ? Evaluating Mathematical Equivalence in Embedding Models
Jiaying Ye, Samarth Rao, Leo Carlin +9
Because mathematics is highly abstract, a single statement can take very different forms depending on what subfield it is framed in. There are many examples where breakthroughs occ…
TheoremGraph: Bridging Formal and Informal Mathematics
Simon Kurgan, Evan Wang, Eric Leonen +6
Mathematical knowledge is organized around statements and their dependencies, but this structure is exposed unevenly: informal papers cite mostly at the document level, while forma…
Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance
Theodore Meek, Siyuan Ge, Di Qiu Xiang +2
Recent work has demonstrated that coding agents can formalize entire advanced mathematics textbooks in Lean 4, yet existing efforts concentrate on branches of mathematics already w…
Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization
Vasily Ilin, Brian Nugent
Large language models can often close proof gaps in interactive theorem provers, but a verified theorem is not the same thing as a reusable library contribution. We study this dist…
CayleyPy-4: AI-Holography. Towards analogs of holographic string dualities for AI tasks
A. Chervov, F. Levkovich-Maslyuk, A. Smolensky +41
This is the fourth paper in the CayleyPy project, which applies AI methods to the exploration of large graphs. In this work, we suggest the existence of a new discrete version of h…
Learning to Repair Lean Proofs from Compiler Feedback
Evan Wang, Simon Chess, Daniel Lee +4
As neural theorem provers become increasingly agentic, the ability to interpret and act on compiler feedback is critical. However, existing Lean datasets consist almost exclusively…