2 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…