10 papers
Formal verification of the S-two AIR
Jeremy Avigad, Anat Ganor, Lior Goldberg +4
StarkWare's S-two prover provides an efficient means for establishing, on blockchain, that a program written in the Cairo virtual machine language runs to completion. The latter cl…
ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization
Riyaz Ahuja, Tate Rowney, Jeremy Avigad +1
Formal mathematics libraries are rapidly expanding, creating a growing need to refactor verified proofs for maintainability and to improve training data quality for neural provers.…
The Future of Artificial Intelligence and the Mathematical and Physical Sciences (AI+MPS)
Andrew Ferguson, Marisa LaFleur, Lars Ruthotto +97
This community paper developed out of the NSF Workshop on the Future of Artificial Intelligence (AI) and the Mathematical and Physics Sciences (MPS), which was held in March 2025 w…
Implementing Dependent Type Theory Inhabitation and Unification
Chase Norman, Jeremy Avigad
Dependent type theory is the foundation of many modern proof assistants. Inhabitation and unification are undecidable problems that are useful for theorem proving and program synth…
DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs
Tate Rowney, Riyaz Ahuja, Jeremy Avigad +1
Domain-specific languages (DSLs) mediate interactions between interactive proof assistants and external automation, but translating between the prover's internal representation and…
Premise Selection for a Lean Hammer
Thomas Zhu, Joshua Clune, Jeremy Avigad +2
Neural methods are transforming automated reasoning for proof assistants, yet integrating these advances into practical verification workflows remains challenging. A hammer is a to…