Cracking selected formal mathematical olympiad problems
A neural theorem prover built for the Lean proof assistant has learned to solve demanding high-school olympiad math problems, including AMC12 and AIME contest problems and two adapted IMO problems. Tr…