OpenAI's Astra Solves More Maths Problems

Astra has solved 10 hard maths problems (published 1 August 2026) following on from its disproof of the Erdös unit distance conjecture (from combinatorial geometry) in May 2026.

A paper of almost 250 pages (inclusive of references) is available from OpenAI's website.

Mathematics in VS Code with Lean

Formalizing mathematics is now possible in VS Code with Lean. See the manual here. Extension here.

Lean functionality is exposed in the UI via the universal quantifier at the top right of VS code.

Consider copying the MIL folder, containing key examples, so you can tinker with the example code.

MIL = Mathematics in Lean.

When you download the MIL, you will see a flurry of activity in your Output Console in VS Code. This will include reams of stuff relating to "Fetching Mathlib build artifact cache" and thousands of file downloads.

You will also see the incantation "lake build" which is the primary build command in the Lean build system.

Advice on how to work through the MIL textbook from the official website - "working through the exercises is central to the experience".

Note: when reading Lean files in VS code turn off Unicode character highlighting (Control-, to get into settings, and update Text Editor settings).

The Lean FRO Year 3 Roadmap

Changes to Lean - as articulated by Lean FRO's Y3 roadmap.  

Some items will for sure be done, some may be pushed to Y4.

All roadmap content can be found here.

While we are there, let's say thank you to the Lean Team.

Theorem Proving in Lean - What Makes Dependent Type Theory Dependent?

This precis is based on the Lean Manual, Section 2.8.

Lean Ecosystem Decoded

elan - package manager for Lean. elan can be used inside VS code and will manage all versions of Lean on your system

Lake - the standard project structure and build system used in Lean

mathlib4 - the math library for LEAN

mathlib4 can be found here. It contains both programmatic infrastructure and mathematics.

Theorem Proving in Lean - Basics of Dependent Type Theory

The master guide is here.

DTT and its Specific Variant for Lean

Dependent type theory (DTT) allows you to express complex mathematical assertions and reason about them in a "natural and uniform" way. 

Lean is based on a version of DTT called the Calculus of Constructions, with a "countable hierarchy of non-cumulative inverses and inductive types". This sounds complex. 

The following section explains this.

First, let's talk Simple Type Theory

In "type theory" every expression has a specific type. e.g. the expression x+0 may denote a natural number in a specific context. In another context, it may be a floating point number, of a particular precision.

In Lean, a natural number is an arbitrary precision unsigned integer.

Our use of the arbitrary precision (unsigned) integer, reflects the unnatural way of thinking about counting numbers from a computing perspective. In computing, we think of the object, but also the memory it occupies - so we speak of 16 bit integers, 32 bit integers and so on - a nod to the physical limitations of computers. n-bit integers where n is not predefined underlies this concept of arbitrary precision.

An arbitrary-precision integer can grow to any number of bits, limited only by available memory. 

This differs from so-called fixed-width integers (8-, 32-, 64- bit).  

A variable-length array of digits/bits are used so it can represent arbitrarily large integers without overflow. (Analogies include - BigInt in Java, or System.Numerics.BigInteger in C#).

Defining Contants in Lean with the def keyword

Let's define some constants in Lean.

/- Define some constants. -/

def  m:  Nat := 1   --m is a natural number

def  n :  Nat := 0

def  b1: Bool := true  --b1 is a Boolean

def  b2: Bool := false

Now check their types using: #check m;  #check n; #check n+0 etc. You can also run some "evals" in Lean: #eval  5*4; #eval m+2 etc.

The def keyword introduces new constant symbols to the working environment. The #check command asks Lean to report their types. The #eval command asks Lean to evaluate the given expression.

Composing New Types from Existing Ones

What makes simple type theory powerful is you can build new types out of others.

For example, if a and b are types, a->b denote the type of functions from a to b, a × b denotes the type of pairs consisting of an element of type a and element of type b.

Note on use of Unicode: (From the Lean Manual): "The judicious use of Unicode improves legibility, and all modern editors have great support for it. In the Lean standard library, you often see Greek letters to denote types, and the Unicode symbol → as a more compact version of ->."

Theorem Proving in Lean - Three Definitions to Get Started

This is an abridged account of Theorem Proving in Lean capturing only the SSPs, or super salient points.

Here are some three starting definitions essential for understanding this topic:

Formal verification - using logical and computational methods to establish claims that are expressed in precise mathematical terms. Example claims - mathematical theorem /hypothesis, claims that pieces of hardware or software, network protocols, security protocols - do what they say they actually do.  The process is "describe your system in mathematical terms" ,then use "theorem proving" to establish truth.

Automated theorem proving - focused on "finding". The "ATP" toolkit includes: resolution theorem provers, tableau theorem provers, fast satisfiability solvers to provide means of establishing validity of formulas in propositional and first-order logic.  Computer algebra systems may be used in concert to carry out mathematical computations.  

Automated reasoning - differs; not as "cast iron" as theorem proving. Automated reasoning is a superset of automated theorem proving, which includes imprecise techniques such as heuristic search and fuzzy logic.

The Lean Programming Language

The Lean Programming language is being used to create a new proof of Fermat's Last Theorem. Some lecture notes from London's Imperial College set the scene.

Theoretical Foundation (DTT)

Dependent type theory (DTT) is the theoretical foundation of Lean (the link provided takes you into the Lean manual and gives a brief intro to the theory) which bears "categorical semantics".

Getting Started with Lean

• The best way to get started in Lean is to read Functional Programming in Lean.
• The next step is to read Theorem Proving in Lean.

Who created Lean

Lean was created by Brazilian computer scientist Leonardo de Moura, in 2013, when he worked in Microsoft Research (where he worked for 16 years). 

Leonardo is now Senior Principal Applied Scientist at AWS, where he works in the Automated Reasoning Group.  This group does a lot of work in Provable Security and Software Assurance.

Lean is available under the Apache 2.0 license.

Leaning in on Lean

Lean is an open-source programming language and proof assistant. AWS uses Lean and "verification-guided development" to verify Cedar, the AWS authorization policy language.

Lean is being used to attempt a computer proof of Fermat's Last Theorem using the blueprint (note: the blueprint link no longer works).