Abstract

Aristotle is an AI theorem prover developed by Harmonic which can autonomously produce multi-thousand-line formal proofs of theorems expressed in Lean 4. It achieved Gold Medal equivalent performance for the 2025 International Mathematical Olympiad (IMO). The Aristotle system takes a Lean theorem without a proof and attempts to find a proof of the theorem (when one exists). The proofs that Aristotle generates are machine checked by the Lean 4 interactive theorem prover, which has the highly desirable property of an LLM -based system that produces an answer without hallucination.

This talk is aimed at a general audience and does not assume much knowledge about interactive theorem provers or hardware design. The first part of this will talk discuss the recent rise in the use of AI theorem provers and present a few high level details about the techniques Aristotle used to tackle hard problems like the IMO challenge e.g. interleaving formal and informal reasoning. The second part of the talk will illustrate how digital hardware can be described using Geraint Jones and Mary Sheeran ’s Ruby relational hardware description language implemented in Lean 4 as an embedded domain specific language. Hardware design in Ruby enjoys many useful algebraic properties and typically involves applying a rich collection of theorems to transform and optimize circuits. This talk will walk through a circuit design example using Ruby, with formally expressed circuit properties automatically proved by Aristotle.

An argument will be made to support the idea that a well curated collection of composable circuit building blocks backed with a rich collection of algebraic properties for circuit transformation forms a solid basis not only for verifying properties of circuits, but also for using machine learning to automatically synthesize correct by construction circuits from specifications.

Bio: Satnam Singh is a software engineer at Harmonic working on the formal verification of hardware and software. He has previously worked on the design of machine learning chips at Google and Groq, orchestration of distributed systems as an early member of the Kubernetes team at Google, the development of tools and techniques for the formal verification of hardware at Xilinx, high level synthesis of hardware at Microsoft, and the optimization of Android applications at Facebook/Meta. https://satnam6502.github.io/bio