@highergeometer@mathstodon.xyz
Post #1365982
2025-05-19 01:58 UTC
@tao @ProfKinyon @xenaproject Well, I learned that this is probably not going to work very well in the online Lean 4 Web version... :-) Getting errors at the first 'lemma' statement (literally the word 'lemma'). Then I switched to 'theorem', and then with LLM advice fiddled with the syntax, and then started having to wrangle the proof itself. At this point I have other things to do, and if I have time I will try to get Lean installed locally (eep) and have another go. I recorded a video of myself but it's not worth sharing.
Replies (1)
-
@tao@mathstodon.xyz 2025-05-19 02:35
@highergeometer @ProfKinyon @xenaproject Thanks for the report. Not as positive as one might have hoped, but negative results are also useful data. I guess LLMs are not good enough yet to get from "only epsilon experience in Lean" to "writing 100-line Lean formalizations" without some serious friction...