We built a neural theorem prover for Lean that learned to unravel quite a lot of difficult high-school olympiad problems, including problems from the AMC12 and AIME competitions, in addition to two problems adapted from the IMO.