Description
An OpenAI model has disproved a central conjecture in discrete geometry [OpenAI, May 2026].” Such headlines from the field of mathematics are increasingly common and reflect a comprehensive effort to “formalize” or “digitalize” [*] mathematics via machine-readable and machine-verifiable proofs, which allows AI models to generate new theorems with their proofs. One of the platforms used is the functional programming language Lean 4 whose dependent type system is used to build up rigorously provable lemmas and theorems. Building on the solid mathematical basis, physicists have been “digitalizing” physics concepts and relationships from classical mechanics up to quantum field theory as part of the PhysLib project. More recently, we have been expanding on this with electron-proton scattering formalisms, DIS kinematics, parton distribution functions, structure functions, and form factors, and their connections to experimental observables. Providing this formally verified foundation creates an un-hallucinable mathematical guardrail for AI agents and allows the EIC community to deploy next-generation AI tools for automated discoveries and robust extractions that are mathematically guaranteed to respect physical laws.
