Post #2522101
2026-05-10 11:53 UTC
@vnikolov@ieji.de
The recent thing was covered by @tao@mathstodon.xyz . The gist is that where there used to be a couple of Erdos problem proof attempts to review per year, there are currently about 1000 ai generated ones. Of the ones that have been formally checked, only the Erdos problem 728 proof has been anything like "useable" (which was produced "mostly by chatgpt by itself" (by a mathematician).). They are all lean proofs.
@kentpitman@climatejustice.social @bagder@mastodon.social
Replies (1)
-
@vnikolov@ieji.de 2026-05-10 12:34
@screwlisp@gamerplus.org In case you have an answer ready: (1) Do I understand correctly that EACH of those thousand or so proofs is represented in the Lean language? If yes: (2.1) Were all those representations produced directly by an LLM, or were they handcrafted from another kind of LLM output? (2.2) Does Lean have all necessary prerequisites to check those proofs as they are? @kentpitman@climatejustice.social @bagder@mastodon.social