Lawrence Wu | Searcharxiv

arXiv2025

Aristotle: IMO-level Automated Theorem Proving

We introduce Aristotle, an AI system that combines formal verification with informal reasoning, achieving gold-medal-equivalent performance on the 2025 International Mathematical Olympiad problems. Aristotle integrates three main components: a Lean proof search system, an informal reasoning system that generates and formalizes lemmas, and a dedicated geometry solver. Our system demonstrates state-of-the-art performance with favorable scaling properties for automated theorem proving.

cs.AI↗

arXiv2016

Pixel Arrays: A fast and elementary method for solving nonlinear systems

We present a new method, called the pixel array method, for approximating all solutions in a bounding box for an arbitrary nonlinear system of relations. In contrast with other solvers, our approach requires that the user must specify which variables are to be exposed, and which are to be left latent. The entire solution set is then obtained---in terms of these exposed variables---by performing a series of array multiplications on the $n_i$-dimensional plots of the individual relations $R_i$. This procedure introduces no false negatives and is much faster than Newton-based solvers. The key is the unexposed variables, which Newton methods can make no use of. In fact, we found that with even a single unexposed variable our method was more than 10x faster than Julia's NLsolve. Due to its relative simplicity, the pixel array method is also applicable to a broader class of systems than Newton-based solvers are. The purpose of this article is to give an account of this new method.

math.NA↗