1
Formally Solving Answer-Construction Problems in Lean
聚焦Lean形式化证明新挑战：提出解决数学竞赛“答案构造”问题的形式化方法，结合LLM进展，拓展自动推理边界。
arXiv:2505.18492v5 Announce Type: replace Abstract: Mathematical competition problems fall into two broad types: theorem proving, which asks for a pro…