2024
Lean Workbook: A large-scale Lean problem set formalized from natural language math problems
NeurIPS 2024poster
Large language models have demonstrated impressive capabilities across various natural language processing tasks, especially in solving mathematical problems. However, large language models are not good at math theorem proving using formal languages like Lean. A significant challenge in this area is…