3 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
Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem
Dustin Bryant, Jim Woodcock, Simon Foster
This paper presents a formalized analysis of the sigmoid function and a fully mechanized proof of the Universal Approximation Theorem (UAT) in Isabelle/HOL, a higher-order logic th…
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.…