Formally Solving Answer-Construction Problems in Lean 事件

Formally Solving Answer-Construction Problems in Lean arXiv:2505.18492v5 Announce Type: replace Abstract: Mathematical competition problems fall into two broad types: theorem proving, which asks for a proof of a given statement, and answer construction, which requires constructing a property-satifying object with proofs. With recent advances in large language models (LLMs), formal theorem-proving techniques have made substantial progress on theorem-proving problems, yet formal answer constructi