Mathematical auto-formalization is emerging as a game-changing outcome of LLMs
and modern AI tools. This is the process of turning mathematical statements in
natural language into fully machine checked proofs. Our problem will
investigate how well these tools actually work by exploring advanced
mathematics and its formalization.