3 papers
cs.LO2026
AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities
Jimmy Xin, Alex Schneidman, Chris Cummins +3
We present AXLE (Axiom Lean Engine), a cloud service for Lean 4 proof manipulation, extraction, and verification. Recent progress in AI for mathematics -- reinforcement learning pi…
cs.SE2026
Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization
Anmol Agarwal, Natalie Neamtu, Pranjal Aggarwal +6
AI coding agents are increasingly used to write real-world software, but ensuring that their outputs are correct remains a fundamental challenge. Formal verification offers a promi…
cs.LO2020
A Novice-Friendly Induction Tactic for Lean
Jannis Limperg
In theorem provers based on dependent type theory such as Coq and Lean, induction is a fundamental proof method and induction tactics are omnipresent in proof scripts. Yet the ergo…