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…
math.NT2026
ABC implies that Ramanujan's tau function misses almost all primes
David Kurniadi Angdinata, Evan Chen, Chris Cummins +21
Lehmer conjectured that Ramanujan's tau-function never vanishes. In a related direction, a folklore conjecture asserts that infinitely many primes arise as absolute values of Raman…
math.CO2026
Dead ends in square-free digit walks
Evan Chen, Chris Cummins, Ben Eltschig +18
We study "dead ends" in square-free digit walks: square-free integers such that, in base , every one-digit extension is non-square-free. In base , the stochastic…