Hacker News new | ask | show | jobs
by michaelfm1211 9 hours ago
Reminds me of this: 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?
1 comments
derdi 9 hours 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
link
xelxebar 6 hours 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.

link
i2talics 2 hours ago
Why does the original C verifier have bugs if its supposedly so easy to implement a verifier?
link
poizan42 1 hour 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.
link