OpenAI:
We built a neural theorem prover for Lean that learned to solve a variety of challenging high-school olympiad problems. These problems are not standard math exercises, they are used to let the best high-school students compete against each other. The prover uses a language model to find proofs of formal statements. Each time we find a new proof, we use it as new training data, which improves the neural network and enables it to iteratively find solutions to harder and harder statements. We achieved a new state-of-the-art (41.2%) on the miniF2F benchmark, a challenging collection of high-school olympiad problems.
DeepMind:
we created a system called AlphaCode that writes computer programs at a competitive level. AlphaCode achieved an estimated rank within the top 54% of participants in programming competitions by solving new problems that require a combination of critical thinking, logic, algorithms, coding, and natural language understanding.





