1 citations · 4 across the 10 of their papers we have counts for
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.…
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…
Hint-Based SMT Proof Reconstruction
Joshua Clune, Haniel Barbosa, Jeremy Avigad
There are several paradigms for integrating interactive and automated theorem provers, combining the convenience of powerful automation with strong soundness guarantees. We introdu…
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…
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…
Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
Yicheng Qian, Joshua Clune, Clark Barrett +1
Proof automation is crucial to large-scale formal mathematics and software/hardware verification projects in ITPs. Sophisticated tools called hammers have been developed to provide…
Canonical for Automated Theorem Proving in Lean
Chase Norman, Jeremy Avigad
Canonical is a solver for type inhabitation in dependent type theory, that is, the problem of producing a term of a given type. We present a Lean tactic which invokes Canonical to…
A Proof-Producing Compiler for Blockchain Applications
Jeremy Avigad, Lior Goldberg, David Levit +2
CairoZero is a programming language for running decentralized applications (dApps) at scale. Programs written in the CairoZero language are compiled to machine code for the Cairo C…