Post #1546530
2026-04-14 02:03 UTC
@regehr I'm a n00b at this stuff but I'm unsurprised. I learnt a little Lean years ago and returned to it recently. I got Codex to generate a proof of a standard theorem. It involves enumeration. It used native_decide to do the enumeration. This is no longer a proof in the Lean kernel. I have to trust the Lean runtime now. That's a whole new level of trust I don't have yet. So thank you for this pointer to precisely what I was worried about!
Replies (1)
-
@regehr@mastodon.social 2026-04-14 02:10
@dpiponi the core problem with formal verification is 100% figuring out what was proved and whether it has any relevance to what you care about