Let's stay in control of mathematics

Mathematical research is about to be drastically accelerated. This will push the classical system of peer review and publishing beyond its limits. We need new, scalable mechanisms for digesting mathematics, or we risk losing control of our field.

Proof assistants like Lean provide a scalable way of ensuring correctness.
Lax builds on this foundation to make formal mathematics scalable for humans too, by organizing results and making them easy to review and reuse.

How it works

Concepts and proofs. Lax annotates natural-language mathematics with Lean. Each definition or claim is tied to a concept: a pair formed by a mathematical statement and a faithful Lean encoding. Each proof is tied to Lean code that derives one concept from others. Concepts and proofs can be reused across submissions.

We study the divisibility of natural numbers. The key step is to find a prime divisor of an arbitrary number greater than one.

Definition 1. A natural number greater than 1 is prime if it is divisible only by 1 and by itself.

Lemma A. Every natural number $n > 1$ has a prime divisor.

Proof. Let $d$ be the least divisor of $n$ with $d > 1$ . Every divisor of $d$ divides $n$ , so $d$ has no divisor strictly between 1 and $d$ ; hence $d$ is prime. $\square$

Theorem B (Euclid). For every $n$ there is a prime $p > n$ .

Proof. By Lemma A, $n! + 1$ has a prime divisor $p$ . If $p \leq n$ , then $p$ divides $n!$ and hence divides 1, which is impossible. So $p > n$ . $\square$

Thus no finite list can contain all the primes: a prime larger than every entry must still exist.

defPrimes

lem✓PrimeDivisor

⊢Proofs.PrimeDivisor
thm✓Euclid
⊢Proofs.Euclid
- lem✓PrimeDivisor
→
thm✓Euclid

Read full introduction to Lax

Throughout this section, graphs are finite and simple. We seek sets of vertices whose pairs are either all edges or all non-edges.

Definition 1. A set $S \subseteq V(G)$ is a clique if any two distinct vertices of $S$ are adjacent, and independent if no two are.

Theorem 2 (Ramsey). For all $a$ and $b$ there is an $N$ such that every graph on at least $N$ vertices contains a clique of size $a$ or an independent set of size $b$ .

Taking $a=b$ gives the symmetric form: every sufficiently large graph contains a clique or an independent set of the prescribed size.

defCliques

thm✓Ramsey

To state a precise running-time bound, we must fix both the machine model and the representation of its input. We use adjacency lists stored in consecutive memory cells.

Definition 1 (Word RAM). A word RAM of word length $w$ has $2^w$ memory cells, each holding a number below $2^w$ , a read-only input tape and a write-only output tape. A program is a finite sequence of instructions [...]; each instruction names the cells it operates on, and arithmetic wraps around modulo $2^w$ . [...]

Definition 2. A graph $G$ on the vertices $0, \ldots, n-1$ with $m$ edges is given to the machine as the word $n, m, o_0, \ldots, o_n, t_0, \ldots, t_{2m-1}$ : the offsets $o_i$ cut the target array $t$ into one block per vertex, and the block of $u$ lists exactly the neighbours of $u$ . [...]

Theorem 3. There are a program and a constant $c$ such that, given any graph as in Definition 2 as a word $x$ , the program halts within $c\,(|x|+1)$ steps having written, for every vertex, the least vertex of its connected component.

Proof. The program scans the vertices in increasing order and runs a breadth-first search from each vertex not yet labelled, labelling everything it reaches with that vertex. [...] Every block of the target array is read once, so the running time is linear in $|x|$ . $\square$

Choosing the least vertex as a component label makes the output independent of the order in which neighbours are explored.

defLax67.Ram

The word RAM

A word RAM is a random access machine whose writable memory consists of $2 ^ w$ cells holding natural numbers below $2 ^ w$ . The word length $w$ is a parameter; one finite program serves all word lengths. Input is a read-only finite array supplied at initialization, also accessible as a sequential tape. Output is an append-only tape. Working memory starts at zero and output starts empty.

The input interface has four operations. $read a$ consumes the next entry of the sequential tape into cell $a$ , halting if the tape is empty. $jeof l$ branches on tape emptiness without consuming input. $inputLength a$ writes the original input length into cell $a$ . $inputLoad a b$ reads the original input at the index in cell $b$ into cell $a$ , returning zero outside the input. Indexed access never consumes the sequential tape, and sequential reads never change the original input. Zero is ordinary data, not an end marker. Each operation costs one instruction. No length header or other framing is added to the supplied list.

Arithmetic results, input values and lengths, output values, and data-memory addresses are reduced modulo $2 ^ w$ . Subtraction is truncated at zero, and division is integer division with $x / 0 = 0$ . Input indices are words too. Program labels and the program counter are natural numbers and are not reduced modulo $2 ^ w$ .

1	import Mathlib.Data.List.Basic
2
	… module docstring, 110 lines
113
114	namespace Lax67.Ram
115
116	/-- An instruction. Every number naming a cell is read, except that
117	the first one names the destination for instructions that write a cell,
118	and the cell holding the destination address for `store`. `set` carries
119	a literal value; `jump`, `jzero`, and `jeof` carry program labels,
120	which are not data-memory addresses. -/
121	inductive Instr
122	/-- Set cell `a` to the literal `n`. -/
123	\| set (a n : ℕ)
124	/-- Set cell `a` to the contents of the cell whose address cell `b`
125	holds. -/
126	\| load (a b : ℕ)
127	/-- Set the cell whose address cell `a` holds to the contents of cell
128	`b`. -/
129	\| store (a b : ℕ)
130	/-- Set cell `a` to the sum of cells `b` and `c`, wrapping around
131	modulo `2 ^ w`. -/
132	\| add (a b c : ℕ)
133	/-- Set cell `a` to the difference of cells `b` and `c`, truncated at
134	zero rather than wrapping around. -/
135	\| sub (a b c : ℕ)
136	/-- Set cell `a` to the product of cells `b` and `c`, wrapping around
137	modulo `2 ^ w`. -/
138	\| mul (a b c : ℕ)
139	/-- Set cell `a` to the quotient of cells `b` and `c`, rounding
140	towards zero; division by zero yields zero. -/
141	\| div (a b c : ℕ)
142	/-- Set cell `a` to the bitwise conjunction of cells `b` and `c`. -/
143	\| and (a b c : ℕ)
144	/-- Set cell `a` to cell `b` shifted left by the number of bits cell
145	`c` holds, wrapping around modulo `2 ^ w`; a shift by `w` or more
146	yields zero. -/
147	\| shiftl (a b c : ℕ)
148	/-- Set cell `a` to the bitwise complement `2 ^ w - 1 - m[b]` of cell
149	`b` within the word length. -/
150	\| not (a b : ℕ)
151	/-- Continue at instruction `l`. -/
152	\| jump (l : ℕ)
153	/-- Continue at instruction `l` if cell `a` is zero. -/
154	\| jzero (a l : ℕ)
155	/-- Continue at instruction `l` exactly when the remaining input tape
156	is empty. This test does not consume input. -/
157	\| jeof (l : ℕ)
158	/-- Write the original input length, reduced to a word, into cell `a`. -/
159	\| inputLength (a : ℕ)
160	/-- Read original input at the word index in cell `b` into cell `a`,
161	returning zero outside the input. Read the index before writing `a`,
162	even when the two cell addresses coincide. Do not consume input. -/
163	\| inputLoad (a b : ℕ)
164	/-- Halt. -/
165	\| halt
166	/-- Read the next number of the input tape into cell `a`, or halt if
167	the tape is exhausted. -/
168	\| read (a : ℕ)
169	/-- Append the contents of cell `a` to the output tape. -/
170	\| write (a : ℕ)
171
172	/-- A program: a finite sequence of instructions, numbered from `0`. -/
173	abbrev Program : Type := List Instr
174
175	/-- A machine state: the program counter, the contents of every memory
176	cell, the immutable original input array, the remaining sequential input
177	tape, and the output tape written so far. -/
178	structure State where
179	/-- The number of the instruction to be executed next. -/
180	pc : ℕ
181	/-- The contents of the memory cells; only the cells with number below
182	`2 ^ w` are ever addressed. -/
183	mem : ℕ → ℕ
184	/-- The original read-only input, unchanged by every instruction. -/
185	input : List ℕ
186	/-- The numbers still to be read from the input tape. -/
187	inp : List ℕ
188	/-- The numbers written to the output tape so far. -/
189	out : List ℕ
190
191	/-- The memory `m` with cell `a` set to `v`, at word length `w`: the
192	address and the value written are both taken modulo `2 ^ w`. -/
193	def setCell (w : ℕ) (m : ℕ → ℕ) (a v : ℕ) : ℕ → ℕ :=
194	fun b => if b = a % 2 ^ w then v % 2 ^ w else m b
195
196	/-- The effect of one instruction on the state at word length `w`, or
197	`none` if it halts the machine, which a `halt` instruction and a read
198	from an exhausted input tape do. Data values, input indices, and
199	data-memory addresses are reduced modulo `2 ^ w`; program labels and
200	the counter are not. -/
201	def Instr.effect (w : ℕ) : Instr → State → Option State
202	\| set a n, s => some { s with pc := s.pc + 1, mem := setCell w s.mem a n }
203	\| load a b, s =>
204	some
205	{ s with
206	pc := s.pc + 1
207	mem := setCell w s.mem a (s.mem (s.mem (b % 2 ^ w) % 2 ^ w)) }
208	\| store a b, s =>
209	some
210	{ s with
211	pc := s.pc + 1
212	mem := setCell w s.mem (s.mem (a % 2 ^ w)) (s.mem (b % 2 ^ w)) }
213	\| add a b c, s =>
214	some
215	{ s with
216	pc := s.pc + 1
217	mem := setCell w s.mem a (s.mem (b % 2 ^ w) + s.mem (c % 2 ^ w)) }
218	\| sub a b c, s =>
219	some
220	{ s with
221	pc := s.pc + 1
222	mem := setCell w s.mem a (s.mem (b % 2 ^ w) - s.mem (c % 2 ^ w)) }
223	\| mul a b c, s =>
224	some
225	{ s with
226	pc := s.pc + 1
227	mem := setCell w s.mem a (s.mem (b % 2 ^ w) * s.mem (c % 2 ^ w)) }
228	\| div a b c, s =>
229	some
230	{ s with
231	pc := s.pc + 1
232	mem := setCell w s.mem a (s.mem (b % 2 ^ w) / s.mem (c % 2 ^ w)) }
233	\| and a b c, s =>
234	some
235	{ s with
236	pc := s.pc + 1
237	mem := setCell w s.mem a (Nat.land (s.mem (b % 2 ^ w)) (s.mem (c % 2 ^ w))) }
238	\| shiftl a b c, s =>
239	some
240	{ s with
241	pc := s.pc + 1
242	mem := setCell w s.mem a (s.mem (b % 2 ^ w) * 2 ^ s.mem (c % 2 ^ w)) }
243	\| not a b, s =>
244	some
245	{ s with
246	pc := s.pc + 1
247	mem := setCell w s.mem a (2 ^ w - 1 - s.mem (b % 2 ^ w)) }
248	\| jump l, s => some { s with pc := l }
249	\| jzero a l, s => some { s with pc := if s.mem (a % 2 ^ w) = 0 then l else s.pc + 1 }
250	\| jeof l, s => some { s with pc := if s.inp.isEmpty then l else s.pc + 1 }
251	\| inputLength a, s =>
252	some { s with pc := s.pc + 1, mem := setCell w s.mem a s.input.length }
253	\| inputLoad a b, s =>
254	some { s with
255	pc := s.pc + 1
256	mem := setCell w s.mem a (s.input[s.mem (b % 2 ^ w) % 2 ^ w]?.getD 0) }
257	\| halt, _ => none
258	\| read a, s =>
259	s.inp.head?.map fun v =>
260	{ s with pc := s.pc + 1, mem := setCell w s.mem a v, inp := s.inp.tail }
261	\| write a, s =>
262	some { s with pc := s.pc + 1, out := s.out ++ [s.mem (a % 2 ^ w) % 2 ^ w] }
263
264	/-- One step of the machine at word length `w`: fetch the instruction
265	the program counter points at and execute it. The result is `none` if
266	the machine has halted, which also happens when the program counter has
267	run past the program. -/
268	def step (w : ℕ) (p : Program) (s : State) : Option State :=
269	p[s.pc]?.bind fun i => i.effect w s
270
271	/-- The state after `t` successful transitions at word length `w`, or
272	`none` if one of those transitions terminates. This auxiliary count does
273	not include a fetched terminal instruction; `RunsTo` charges that too. -/
274	def run (w : ℕ) (p : Program) : ℕ → State → Option State
275	\| 0, s => some s
276	\| t + 1, s => (step w p s).bind (run w p t)
277
278	/-- The initial state on input `x`: program counter zero, all memory
279	cells zero, the original input array and its sequential tape both `x`,
280	and the output tape empty. -/
281	def initState (x : List ℕ) : State where
282	pc := 0
283	mem := fun _ => 0
284	input := x
285	inp := x
286	out := []
287
288	/-- Cost of termination at `s`, when `step w p s = none`: a fetched
289	terminal instruction costs one, while an out-of-range program counter
290	costs zero because there is no instruction to execute. -/
291	def terminalCost (p : Program) (s : State) : ℕ :=
292	if s.pc < p.length then 1 else 0
293
294	/-- Started on input `x` at word length `w`, the machine executes
295	exactly `t` instructions and then halts, having written the word `y` to
296	its output tape. -/
297	def RunsTo (w : ℕ) (p : Program) (x y : List ℕ) (t : ℕ) : Prop :=
298	∃ (k : ℕ) (s : State), run w p k (initState x) = some s ∧
299	step w p s = none ∧ s.out = y ∧ t = k + terminalCost p s
300
301	end Lax67.Ram
302

defLax11.GraphEncoding

Compressed sparse row encoding of a graph

A graph is handed to a word random access machine as a word of numbers in compressed sparse row form, the adjacency-array format every textbook assumes: the number n of vertices, the number m of edges, then n+1 offsets, then the target array. The target array lists, for each vertex in turn, the neighbors of that vertex; the offsets say where each vertex's block of neighbors begins, the first offset being 0 and the last one the length of the target array. So the neighbors of vertex u are the entries of the target array at the positions from the u-th offset up to, but excluding, the (u+1)-st.

1	import Mathlib.Combinatorics.SimpleGraph.Basic
2
	… module docstring, 48 lines
51
52	namespace Lax11.GraphEncoding
53
54	/-- The number of vertices declared by a word: its first entry. -/
55	def vertexCount (x : List ℕ) : ℕ := x.getD 0 0
56
57	/-- The number of edges declared by a word: its second entry. -/
58	def edgeCount (x : List ℕ) : ℕ := x.getD 1 0
59
60	/-- The `i`-th offset of a word: the `n+1` offsets follow the two
61	header entries. -/
62	def offset (x : List ℕ) (i : ℕ) : ℕ := x.getD (2 + i) 0
63
64	/-- The `j`-th entry of the target array of a word, which follows the
65	header and the offsets. -/
66	def target (x : List ℕ) (j : ℕ) : ℕ := x.getD (3 + vertexCount x + j) 0
67
68	/-- The word `x` is a compressed sparse row encoding of the graph `G`
69	on `n` vertices. -/
70	structure EncodesGraph (x : List ℕ) (n : ℕ) (G : SimpleGraph (Fin n)) :
71	Prop where
72	/-- The word declares `n` vertices. -/
73	vertexCount_eq : vertexCount x = n
74	/-- The word consists of the two header entries, the `n+1` offsets,
75	and a target array of length twice the declared number of edges. -/
76	length_eq : x.length = 3 + n + 2 * edgeCount x
77	/-- The block of the first vertex begins at the start of the target
78	array. -/
79	offset_zero : offset x 0 = 0
80	/-- The block of the last vertex ends at the end of the target
81	array. -/
82	offset_last : offset x n = 2 * edgeCount x
83	/-- The offsets are nondecreasing, so they cut the target array into
84	one block per vertex. -/
85	offset_mono : ∀ i < n, offset x i ≤ offset x (i + 1)
86	/-- Every entry of the target array is a vertex. -/
87	target_lt : ∀ j < 2 * edgeCount x, target x j < n
88	/-- The block of a vertex lists exactly its neighbors. -/
89	adj_iff : ∀ u v : Fin n, G.Adj u v ↔
90	∃ j, offset x u ≤ j ∧ j < offset x (u + 1) ∧ target x j = v
91
92	end Lax11.GraphEncoding
93

thm✓Lax11.ConnectedComponents

⊢Lax11Proofs.CCMain.exists_linearTime_program_ccLabels

Proof network. Explore how proofs compose and which claims are proven. Any later submission can discharge an open obligation, and every result that rested on it is then proven.

assumptions conclusionProven claimStatement 1, 2, … of a claim with several statementsClaim from this submissionProof — open large view for details

Get started right away

Set up, once per machine:

npm install -g lax-archive && lax doctor

First, open PowerShell as administrator and install a Linux terminal with WSL:

wsl --install

After restarting, open Ubuntu.

Set up, once per machine:

npm install -g lax-archive
lax doctor

Hand your coding agent a prompt like:

Run `lax print instructions` and follow the guide to formalize <my result>.

Then your agent takes over and guides you through the process.

Community and Feedback

Join the conversation

Lax is shaped by the people who use and review it. Join the Lax Discord to ask questions, exchange ideas, and share feedback, or email us at lax.lean.archive@gmail.com. You can also meet the community at the Lax Online Meeting.

Build foundations together

Concepts are shared across submissions. Below are some definitions other submissions already build on.

Submissions

65 submissions · 685 concepts · 601 statements, 574 proven

Browse by topic

Environments first, then topics suggested from submission and concept titles.

Showing all 65 submissions.

FAQ

How do I create my own submission?

Contributing is a two-step process. Set up once per machine with npm install -g lax-archive followed by lax doctor, then hand your coding agent a prompt such as "Run lax print instructions and follow the guide to formalize <my result>." See Getting started for what happens at each step.
How does Lax relate to Merely True, Tau Ceti, Lean Pool, and the Palomar Registry?

In Merely True and Tau Ceti, individual contributions blend into a shared library. Lax keeps each submission as a distinct, citable unit. This is closer to academic publishing culture: a submission can be cited directly or attached to a conference or journal submission for review, anonymously if needed.

Like Lean Pool and the Palomar Registry, Lax archives individual submissions. The important difference is that Lax submissions can build on one another. A base submission might define a concept such as treewidth, the RAM model, game semantics, or an orbifold. Following submissions can import it instead of reformalizing it and asking the community to vet the same definition again.
How can Lax help with conference and journal review?

A paper accompanied by a Lax submission gives reviewers a shorter route to checking that its formal statements are correct. Lax exposes the semantic closure of each statement: a minimal set of declarations that fully specifies it. Reviewers can therefore focus their limited time on the ideas and techniques.
Can I use Lax for anonymous peer review?

Yes. Set anonymous: true in manifest.yaml and submit as usual. The site then withholds author names, the citation, the bibliography, and every link to your source repository. This is presentation-level anonymity compatible with light double-blind review. The repository and your work stay public.
Can I work on two submissions in parallel locally?

Yes. If one depends on the other, its pinned require must match the dependency's archive record, so every edit to the dependency would otherwise need a submit first. Instead, keep both in one repository and add a Lake package override in .lake/package-overrides.json that points the dependency's package name at the sibling folder. Plain lake build then reads the working tree while the pin stays untouched. When the dependency is ready, submit it, update the pin, and run lax build, which rebuilds from the pins alone.
Why are files, not declarations, the basic unit of Lax?

Because many mathematical concepts cannot be expressed in a single declaration. Treewidth, for example, needs a structure for tree decompositions, a definition of their width, and a definition of the parameter as a minimum over them. These only make sense together, and a reader vetting the definition needs to see all of them. Lax therefore treats the file as the atomic unit of a concept.
What if I can only formalize my paper's content, not its large dependencies?

State each result you rely on as a concept without a proof. You can leave it as an open obligation of your own submission, or put it in a separate concept-only submission dedicated to that result.
Which operating systems does Lax support?

Lax is tested on Linux and macOS. On Windows, use the Windows Subsystem for Linux (WSL). Native Windows support is not currently tested.
Does my submission need to be hosted on GitHub?

No. Lax accepts submissions hosted on GitHub, GitLab.com, Codeberg, and Bitbucket Cloud. If your preferred Git host is missing, please contact us.
How do dependencies stay compatible as mathlib changes?

Submissions that build on one another need compatible Lean, mathlib, and other dependency versions. Lax therefore plans to use long epochs that freeze those versions across the archive. When a new epoch is needed, the community can carry useful submissions forward based on demand. Epoch length will follow how the archive and its community evolve.
Won't publishing formalizations accelerate loss of control of mathematics?

Published formalizations can be used to autonomously prove new theorems. However, we believe the benefits of maintaining these formalizations within our community, and using them to understand new mathematics, outweigh the risks.

1	import Mathlib.Data.Nat.Notation
2
3	namespace Primes
4
5	/-- `n` is prime: it is greater than 1, and its only divisors are 1 and `n`
6	itself. -/
7	def Prime (n : ℕ) : Prop :=
8	1 < n ∧ ∀ d, d ∣ n → d = 1 ∨ d = n
9
10	end Primes
11

1	import Primes
2
3	namespace PrimeDivisor
4	open Primes
5
6	/-- Every natural number greater than 1 has a prime divisor. -/
7	axiom exists_prime_dvd : ∀ n : ℕ, 1 < n → ∃ p, Prime p ∧ p ∣ n
8
9	end PrimeDivisor
10

1	import Primes
2
3	namespace Euclid
4	open Primes
5
6	/-- Beyond every natural number lies a prime. -/
7	axiom exists_prime_gt : ∀ n : ℕ, ∃ p, Prime p ∧ n < p
8
9	end Euclid
10

1	import Mathlib.Combinatorics.SimpleGraph.Basic
2
3	namespace Cliques
4
5	variable {V : Type*} (G : SimpleGraph V)
6
7	/-- Any two distinct vertices of `S` are adjacent. -/
8	def IsClique (S : Set V) : Prop :=
9	∀ u ∈ S, ∀ v ∈ S, u ≠ v → G.Adj u v
10
11	/-- No two vertices of `S` are adjacent. -/
12	def IsIndepSet (S : Set V) : Prop :=
13	∀ u ∈ S, ∀ v ∈ S, ¬ G.Adj u v
14
15	end Cliques
16

1	import Cliques
2	import Mathlib.Data.Set.Card
3
4	namespace Ramsey
5	open Cliques
6
7	/-- Ramsey's theorem: a large enough graph contains a clique on `a`
8	vertices or an independent set on `b` vertices. -/
9	axiom exists_clique_or_indepSet (a b : ℕ) :
10	∃ N : ℕ, ∀ (n : ℕ) (G : SimpleGraph (Fin n)), N ≤ n →
11	(∃ S : Set (Fin n), IsClique G S ∧ a ≤ S.ncard) ∨
12	(∃ S : Set (Fin n), IsIndepSet G S ∧ b ≤ S.ncard)
13
14	end Ramsey
15

Lax Lean Archive