Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification.

arXiv:2609.11319v2 Announce Type: replace Abstract: Most of mathematical knowledge has been communicated through so-called informal use of mathematics and natural language. With large language models (LLMs) being highly adept in using natural language, they ac