Post #1365981
2025-05-18 22:02 UTC
@highergeometer @ProfKinyon @xenaproject That actually makes your experiment particularly valuable... I suspect that these LLM tools are more helpful for beginners in Lean than for those already expert in the syntax and methods... as long as they are used to assist one's learning of the language, rather than as a replacement for that learning. Anyway, will be very interested in reading how things go.
Replies (1)
-
@highergeometer@mathstodon.xyz 2025-05-19 01:58
@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.