Lawrence C Paulson opens his chronology by dismissing the claim, voiced by Peter Thiel and assorted YouTube influencers, that science has stagnated for 50 years. His counterexample is his own field: LCF-style proof assistants.

The story starts in 1975 with Edinburgh LCF, Robin Milner's system announced at the Arc-et-Senans conference. It established the pattern still used today: a proof kernel encapsulated in an abstract type in ML, so that only inference rules can produce values of type thm. It introduced natural-deduction rules, goal-directed proof with tactics and tacticals, and structured theories. The logic was tiny, just universal quantification, conjunction and implication, with no negative numbers or decimal notation. Paulson joined Milner and Mike Gordon in Cambridge in 1982, rewrote much of the system into Cambridge LCF, and verified the unification algorithm in 36 inductions.

From 1985 to 1995, Cambridge LCF's faster ML compiler fed into Gordon's HOL88, and hardware verification became real: production chip designs were verified while software verification lagged. Isabelle development began in 1986, written in Standard ML. The calculus of inductive constructions emerged, the formalism behind today's Rocq and Lean. Isabelle/HOL first appeared in 1991, largely Tobias Nipkow's work.

The 1994 Pentium FDIV bug, which cost Intel nearly half a billion dollars in recalls, pushed John Harrison into floating-point verification. His 1996 thesis formalised real analysis in HOL: metric spaces, limits, differentiation, integration, IEEE-based floating-point proofs. Automation improved too, with Hurd's Metis prover and Isabelle's simplifier. Proof General gave several systems a common Emacs interface.

By 2005 the field had landmark results: Gonthier's Coq proof of the Four Colour Theorem, Avigad's formalisation of the Prime Number Theorem in Isabelle, and the ARM6 processor verification by Gordon, Birtwistle and Fox. Isabelle gained the Isar proof language, type classes, counterexample finders and code generation.

The decade after 2005 brought seL4, the first formally verified OS kernel, now backed by a million lines of Isabelle/HOL proofs. CompCert delivered a verified compiler for a large C subset, and CakeML closed the bootstrapping circle with a verified compiler down to assembly. Mathematics followed: Gödel's second incompleteness theorem, the Central Limit Theorem, the Flyspeck project and the odd order theorem were all formalised.

The last decade broke into mainstream mathematics, driven by Kevin Buzzard's promotion of Lean. In 2022 machine assistance confirmed new mathematics that a Fields Medallist had doubted. In industry, Isabelle contributed to the CHERI capability architecture and to WebAssembly's specification, where Conrad Watt found fixable issues. On 4 December 2025 AWS announced the Nitro Isolation Engine for Graviton5: a Rust separation kernel with 260,000 lines of Isabelle/HOL proofs covering confidentiality and integrity, a project Paulson himself works on.

His closing analogy: smartphones were once revolutionary and now draw no crowds. Formal verification is not ordinary yet, but it is heading there.