@highergeometer@mathstodon.xyz
Post #1365980
2025-05-18 21:59 UTC
@tao @ProfKinyon @xenaproject thanks! I've used Claude to grind down big, multi-case Isabelle proofs before, but my actual Lean experience is epsilon.
Replies (1)
-
@tao@mathstodon.xyz 2025-05-18 22:02
@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.