Post #4445801

2026-07-21 17:36 UTC

Or maybe more briefly: When doing AI-assisted programming, it sometimes happens that people have the AI generate both the code and its tests, and then discover that although the tests pass because code and tests match, both diverge from the specification of what the AI claimed its code would actually do? How do we know this didn't happen with the 1.2 million lines of Lean that purport to be validating the solution to the Erdős unit distance problem? Couldn't they be a 100% correct verification of the wrong theorem?

Replies (2)

@pozorvlak@mathstodon.xyz 2026-07-21 17:39

@mjd@mathstodon.xyz do you actually need to check all the imported definitions? Or just the ones used in the headline theorem?

Open ##4445802
@highergeometer@mathstodon.xyz 2026-07-22 01:54

@mjd@mathstodon.xyz The statement of the main theorem itself (and its required definitions) here is not that long and can be read, parsed and verified by a human reader. Mathlib is heavily curated and trusted. There are tools that check that a) no new 'magic axioms' were introduced b) no external untrustworthy sources are used as black boxes (you can import pre-calculated results in Lean for instance, to my knowledge, since it is a general programming language). There are even more adversarial checking frameworks that can be set up. People who work in Lean are very aware of the potential abuses and misuses, and work on ways to detect such things, @xenaproject@mathstodon.xyz is well aware of how these things work, and is always pushing people who turn up in the Lean Zulip chat server with AI-generated Lean projects to use best practices that adhere to such a checking regime. Not to mention giving many talks over the years that mention the problem you say about misformalised statements.

Open ##4445806