Tootfinder

Interesting viewpoint on #leanprover and encoding pure math in type theory that @… just pointed me to:
https://mathoverflow.net/questions/513540/should-we-trust-ai-generated-formal-proofs-in-lean-4/513585#513585
In-type junk values are another extremely efficient footgun when working with proof assistants.

If somebody posts a claimed #AI generated proof of the Riemann hypothesis on the arXiv and it has a complete #lean formalization coming with the paper, would you download the lean proof (~100.000 lines) and check it on your computer?
You should NOT DO THIS.
That's very easy social engineering because you just downloaded code from the Internet and ran it. Could be malware.