Yes, 50 years of LCF would have been much better. You should not talk about "50 years of proof assistants" and not mention Mizar which had the largest library of theorems for about half of that time.
Isabelle/HOL is still types. The underlying type theory of Isabelle/HOL is not theory of dependent types, but theory of simple types.
Isabelle/ZF would be a better example as it encodes Zermelo–Fraenkel set theory.
The example papers [1] [2] [3] [4] have 18 unique co-authors. Also, it's Beatriz.
> she makes analysis of several pairs of pictures
"We base our analysis on the catalog of 298,165 short-duration transients presented in Solano et al. (2022), detected in 200 red POSS-I plates with typical exposure times of 45–50 minutes." [1]
"Of the 2,718 days in this period, transients were observed on 310 days (11.4%)" [2]
"These searches significantly reduced the number of candidates (from 298 165 to 9 395)" [3]
> uniformly spread out across the whole plate
> thousands of uniformly spread out image defects
"we find a strong deficit of transient detections, at the 22 sigma statistical significance level, within the Earth’s umbral shadow" [1]
"we expect N = 1223 transients in shadow out of 106,339 total, corresponding to an expected fraction of fexp = 0.0115±0.00033. However, we observe only N = 349 transients in shadow" [1]
"Plate defects, by contrast, are expected to be randomly shaped and distributed" [1]
> in all pairs of plates the lights change one way only. On the first plate they are present and on the next plate 50 minutes later they disappear
"transients that appear only in one long exposure and are entirely absent shortly before and after" [1]
"In brief, transients were defined as distinct star-like point sources present in POSS-I E Red images that were absent both in images taken immediately prior to the POSS-I Red image and in all subsequent images." [2]
(*) POSS -- Palomar Observatory Sky Survey
[1] Aligned, multiple-transient events in the First Palomar Sky Survey, 2025, preprint
[2] Transients in the Palomar Observatory Sky Survey (POSS-I) may be associated with nuclear testing and reports of unidentified anomalous phenomena, Scientific Reports, 2025
[3] Discovering vanishing objects in POSS I red images using the Virtual Observatory, 2022, Monthly Notices of the Royal Astronomical Society, 515, 1380
[4] A glint in the eye: photographic plate archive searches for non-terrestrial artefacts, 2022, Acta Astronautica, 194, 106
Turns out looking for quotes directly contradicting debunker's statements is a great way to focus while reading a UAP-related scientific paper, thank you.
The purpose of math is indeed to increase our understanding, but the correctness of proofs is a precondition for that. A wrong proof does not increase understanding, although it may create such illusion.
Proof assistants provide scalability to correctness checking and this way they contribute to understanding.
Some proof assistants contribute more directly to understanding by making proofs easier to study.
Indeed. Strange that the previous commenter attacked such an obvious strawman ... they responded to my statement about the purpose of proof with a statement about the purpose of math, which I hadn't mentioned. Also strange is the claim that the purpose of a proof is to show "why" a statement is true rather than that a statement is true. Some proofs help understand the "why" but many don't (proofs of the FLT included) and informal discussion is usually better for that, and is often why we believe that an unproven proposition is true -- e.g., it's widely believed, for good reasons, that P != NP, but no one knows how to prove it. Ditto for the Collatz conjecture.
Isabelle is a generic theorem prover. It supports the standard set theory on first order logic as well, but it's most popular logic is HOL, which is a kind of type theory. Isabelle is well integrated with LaTeX, so its support for mathematical symbols goes beyond unicode. One can write complete well typeset mathematical papers inside Isabelle, and people do. So it's not that. Yet, the dynamics of Lean uptake among mathematicians is much better, so I am curious why is that. I would really like to see an opinion of someone who knows both Lean and Isabelle well, but prefers Lean for formalized mathematics. Or is that all coincidence and hype?
I am talking not about the ability to typeset your proofs, but the source code itself for the proofs. At the very least all the Isabelle and Coq proofs I've looked at have look much more like source code than the proofs they formalize.
The title is quite misleading. This is a tutorial on reading a Lean verification script so the title should be like "Anatomy of a Lean verification script". As it is it suggests that all formal proofs look like this which they typically don't.
The title seems quite apt in my opinion. The article describes a proof as does the title. It doesn’t claim that all proofs are like this. The title isn’t “The anatome of formal proofs” or “all formal proofs” or anything similar.
Isabelle proving environment implements this idea since at least 2005 when I started using it. One can interleave formal proofs and informal commentary in a theory file and one of the artifacts is a "proof document" that is a result of LaTeX processing of the file. Other options exist as well where the file is exported to HTML with hyperlinks to theorems and definitions referenced in a proof. There are also custom HTML renderers (since 2008) where a reader can expand parts of the structured proof when they want to see more details.
Agda 1 (more specifically, the included UI program known as Alfa) implemented an automated translation from formal proof to natural language, driven via Grammatical Framework. This requires writing snippets of code to translate every single part of the formal language to its natural language equivalents, at varying levels of verboseness - for example, (add ab) could become "a + b", "the addition of a and b", "adding b to a" and so on. Similar for proof steps such as "We proceed by induction on n", properties such as "is commutative" etc. The idea gets reimplemented every now and then, in a variety of systems. Of course the most compelling feature is being able to "expand out" proof steps to any desired level of detail.
