Post #1365983
2025-05-19 02:35 UTC
@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...
Replies (2)
-
@highergeometer@mathstodon.xyz 2025-05-19 03:25
@tao @ProfKinyon @xenaproject It may well be the fact that I was working with a slightly crippled system. I couldn't get Lean 4 Web to import all the tactics you did in your example video where you tackled that other Equational implication.
-
@Lavendula@mathstodon.xyz 2025-05-19 17:44
@tao @highergeometer @ProfKinyon @xenaproject It's terrible that when I ask some questions in zulip, there might be someone tells me do not use LLM......