@highergeometer@mathstodon.xyz
Post #1365978
2025-05-18 21:52 UTC
@ProfKinyon @tao @xenaproject I might have a go using the fun and slightly naive approach of coercing a LLMs to try their hand, if I had a copy of your proof.
Replies (1)
-
@tao@mathstodon.xyz 2025-05-18 21:58
@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!