Post #1365979
2025-05-18 21:58 UTC
@highergeometer @ProfKinyon @xenaproject It’s now posted at https://leanprover.zulipchat.com/#narrow/channel/219941-Machine-Learning-for-Theorem-Proving/topic/A.20.28semi.29-autoformalization.20challenge.3A.20650.3D.3E448. Would be interested in seeing a report on your LLM-assisted formalization as a further data point for the thread!
Replies (1)
-
@highergeometer@mathstodon.xyz 2025-05-18 21:59
@tao @ProfKinyon @xenaproject thanks! I've used Claude to grind down big, multi-case Isabelle proofs before, but my actual Lean experience is epsilon.