3 ms·

Reminds me of this: https://mathoverflow.net/questions/513742/are-we-stuck-with-lean https://mathoverflow.net/questions/513742/are-we-stuck-with-... I know thi

Reminds me of this: https://mathoverflow.net/questions/513742/are-we-stuck-with-lean https://mathoverflow.net/questions/513742/are-we-stuck-with-... I know this is an implementation bug not a meta-theory bug, but I'd almost consider the fact soundness bugs are possible as a bug in the ideology, or at least a severe drawback. Stuff like this just wouldn't happen in Metamath. In a future where AI is autogenerating formalizations, why not have the AI use a harder but airtight system like Metamath?

derdi 2mo ago
Took me about 90 seconds to find a Metamath implementation bug that apparently allowed proving something that shouldn't be provable: https://github.com/metamath/metamath-exe/issues/184 https://github.com/metamath/metamath-exe/issues/184
- xelxebar 2mo ago
  That's with the original C verifier only. The actual database is cross-checked by 6 independent implementations. This is the whole point of Metamath: its kernel is so tiny that you can implement a verifier in a weekend. Metamath isn't a silver bullet in the design space of formal proof tools, but I personally think it just about nails the metatheory we want. Maybe some explicit facility around definitions would be desireable.
  - i2talics 2mo ago
    Why does the original C verifier have bugs if its supposedly so easy to implement a verifier?
    - poizan42 2mo ago
      Nothing more complex than Hello world is easy to implement in C without risking mistakes in checking boundary conditions if you are not really careful.
    - xelxebar 2mo ago
      Ease of implementation means we get more, independent verifiers rather than trusting any particular one.
  - LegionMammal978 2mo ago
    As it happens, the Python verifier mmverify.py has an even simpler soundness bug [0], and so far I've reviewed two independent AI-written verifiers that have replicated that bug, since they apparently really like to copy the strategy from mmverify.py. A sound verifier isn't too difficult to write in terms of architecture (I just wrote one myself for differential testing [1]), but it requires some close attention to the details. That is to say, the Swiss-cheese approach definitely lends authority, but individual implementations are unfortunately not as foolproof as they're made out to be. [0] https://github.com/david-a-wheeler/mmverify.py/issues/30 https://github.com/david-a-wheeler/mmverify.py/issues/30 [1] https://github.com/LegionMammal978/mm-verifier-tests/blob/main/mmreference.py https://github.com/LegionMammal978/mm-verifier-tests/blob/ma...
alethic 2mo ago
The utility of autoformalization is not actually in confirming the correctness of human-checked results. Mathematicians have a pretty good peer review process. I'm not actually aware offhand of any mathematical results that were accepted and later found to be incorrect -- though I'm sure cases exist, it's astoundingly rare. The mathematics community's motivation for formalizing problems like Maryna Viazovska's sphere packing results in Lean weren't because the results were in doubt -- she won a Fields Medal for it, it's an extremely examined proof -- but because formalizing those results would lead to a lot of interesting and useful mathematical objects needing to be formalized as a prerequisite, which could then be merged into Lean's Mathlib and become useful for anyone working with Lean, particularly students. Having a library of idiomatic proofs available in a formal system capable of checking your work is Really Cool! Working in a proof assistant is a great way to develop mathematical maturity, especially for people who might not have an undergraduate education available to them. (Unfortunately in the sphere packing case, the research group working on it made the mistake of trusting one of the various "AI for Math" slop companies, who promptly rugpulled them: https://arxiv.org/html/2603.03684v3 https://arxiv.org/html/2603.03684v3) So the short answer is "it depends on what you want". Lean is an eminently usable system for humans and LLMs alike; Metamath is uh. Not. But yes, Metamath seems to have a more trustable kernel wrt. the independent verifiers, so if that's all you're after it would be a better pick. But... there's only so many bugs Lean's kernel can have. At some point, they'll all be found.
- senderista 2mo ago
  > I'm not actually aware offhand of any mathematical results that were accepted and later found to be incorrect https://mathoverflow.net/questions/35468/widely-accepted-mathematical-results-that-were-later-shown-to-be-wrong https://mathoverflow.net/questions/35468/widely-accepted-mat...
  - jojomodding 2mo ago
    Yes, in particular the slides by Kevin Buzzard (linked in there or here: https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/slides/fomm_buzzard.pdf https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/sli... ) are funny and educational on that matter.

derdi 2mo ago

Took me about 90 seconds to find a Metamath implementation bug that apparently allowed proving something that shouldn't be provable: https://github.com/metamath/metamath-exe/issues/184 https://github.com/metamath/metamath-exe/issues/184

xelxebar 2mo ago
That's with the original C verifier only. The actual database is cross-checked by 6 independent implementations. This is the whole point of Metamath: its kernel is so tiny that you can implement a verifier in a weekend. Metamath isn't a silver bullet in the design space of formal proof tools, but I personally think it just about nails the metatheory we want. Maybe some explicit facility around definitions would be desireable.
- i2talics 2mo ago
  Why does the original C verifier have bugs if its supposedly so easy to implement a verifier?
  - poizan42 2mo ago
    Nothing more complex than Hello world is easy to implement in C without risking mistakes in checking boundary conditions if you are not really careful.
  - xelxebar 2mo ago
    Ease of implementation means we get more, independent verifiers rather than trusting any particular one.
- LegionMammal978 2mo ago
  As it happens, the Python verifier mmverify.py has an even simpler soundness bug [0], and so far I've reviewed two independent AI-written verifiers that have replicated that bug, since they apparently really like to copy the strategy from mmverify.py. A sound verifier isn't too difficult to write in terms of architecture (I just wrote one myself for differential testing [1]), but it requires some close attention to the details. That is to say, the Swiss-cheese approach definitely lends authority, but individual implementations are unfortunately not as foolproof as they're made out to be. [0] https://github.com/david-a-wheeler/mmverify.py/issues/30 https://github.com/david-a-wheeler/mmverify.py/issues/30 [1] https://github.com/LegionMammal978/mm-verifier-tests/blob/main/mmreference.py https://github.com/LegionMammal978/mm-verifier-tests/blob/ma...

alethic 2mo ago

The utility of autoformalization is not actually in confirming the correctness of human-checked results. Mathematicians have a pretty good peer review process. I'm not actually aware offhand of any mathematical results that were accepted and later found to be incorrect -- though I'm sure cases exist, it's astoundingly rare. The mathematics community's motivation for formalizing problems like Maryna Viazovska's sphere packing results in Lean weren't because the results were in doubt -- she won a Fields Medal for it, it's an extremely examined proof -- but because formalizing those results would lead to a lot of interesting and useful mathematical objects needing to be formalized as a prerequisite, which could then be merged into Lean's Mathlib and become useful for anyone working with Lean, particularly students. Having a library of idiomatic proofs available in a formal system capable of checking your work is Really Cool! Working in a proof assistant is a great way to develop mathematical maturity, especially for people who might not have an undergraduate education available to them. (Unfortunately in the sphere packing case, the research group working on it made the mistake of trusting one of the various "AI for Math" slop companies, who promptly rugpulled them: https://arxiv.org/html/2603.03684v3 https://arxiv.org/html/2603.03684v3) So the short answer is "it depends on what you want". Lean is an eminently usable system for humans and LLMs alike; Metamath is uh. Not. But yes, Metamath seems to have a more trustable kernel wrt. the independent verifiers, so if that's all you're after it would be a better pick. But... there's only so many bugs Lean's kernel can have. At some point, they'll all be found.

senderista 2mo ago
> I'm not actually aware offhand of any mathematical results that were accepted and later found to be incorrect https://mathoverflow.net/questions/35468/widely-accepted-mathematical-results-that-were-later-shown-to-be-wrong https://mathoverflow.net/questions/35468/widely-accepted-mat...
- jojomodding 2mo ago
  Yes, in particular the slides by Kevin Buzzard (linked in there or here: https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/slides/fomm_buzzard.pdf https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/sli... ) are funny and educational on that matter.