2 papers
cs.AI2026
Munkres' General Topology Autoformalized in Isabelle/HOL
Dustin Bryant, Jonathan Julián Huerta y Munive, Cezary Kaliszyk +1
We describe an experiment in LLM-assisted autoformalization that produced over 85,000 lines of Isabelle/HOL code covering all 39 sections of Munkres' Topology (general topology, Ch…
cs.LO2025
Verifying Numerical Methods with Isabelle/HOL
Dustin Bryant, Jonathan Julian Huerta y Munive, Simon Foster
Modern machine learning pipelines are built on numerical algorithms. Reliable numerical methods are thus a prerequisite for trustworthy machine learning and cyber-physical systems.…