1.1k citations · 7.8k across the 180 of their papers we have counts for
Showing 2026Show all
2 papers · 1 filter
cs.LO2026
FloatLib: Verified Floating-Point Arithmetic in Lean
Robert Joseph George, Will Adkisson, Anima Anandkumar
We present FloatLib, a verified arbitrary-precision floating-point arithmetic library in Lean 4 that combines broad format coverage, machine-checked correctness, and efficient cert…
cs.AI2026
ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers
Jiayi Wu, Robert Joseph George, Anima Anandkumar
Formal theorem proving has emerged as a frontier challenge for machine learning, yet the ecosystem is fragmented: proofs remain siloed across incompatible systems, limiting both tr…