HN user
I do formalized mathematics as a hobby, see https://github.com/SKolodynski/IsarMathLib
Mizar is an early theorem prover. It still exists, see the 2025 issue of Formalized Mathematics journal [1] that publishes math articles formally verified by Mizar (since 1990).
Mizar source was "available upon request" for maybe 30-40 years. It got completely open-sourced under GPL some 3 years ago (maybe earlier, not sure), see [1], also [2] and [3] about an alternative implementation in Rust. Mizar is indeed "scarcely advertised", but all the information is publicly available, who wants to know knows. As for Mizar semantics, see for example [4].
[1] https://github.com/MizarProject/system [2] https://github.com/digama0/mizar-rs [3] https://arxiv.org/pdf/2304.08391v2 [4] https://link.springer.com/article/10.1007/s10817-018-9479-z
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.
It's about surreal numbers https://en.wikipedia.org/wiki/Surreal_number
There are "1498 articles written by 278 authors and 73460 theorems, 14291 definitions" at http://mmlquery.mizar.org/
one scientist, Beatrice Villarroel
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.
There was a question [1] on mathoverflow about this with a couple of interesting answers and comments.
[1] https://mathoverflow.net/questions/291158/proofs-shown-to-be...
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.
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?
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.
No need to wonder for long, just have a look.
Metamath: https://us.metamath.org/mpeuni/mmset.html#axioms
Isabelle/ZF: https://isabelle.in.tum.de/dist/library/FOL/ZF/ZF_Base.html
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.
A more sensibly formulated question would be "What is your estimation of probability that some UFO's (or UAP's) are technological objects created by a non-human intelligence?".
A bit of history: Sledgehammer became fully operational in 2007, extended to call external SMT solvers in 2008. Looks like Lean is catching up.
According to Christopher Mellon the radar data and deck logs from USS Nimitz and Princeton from the time of 2004 incident are "missing", see https://youtu.be/UdIhhYkMG2Y?t=1330 .
The first one is not a select but syntax for defining a small in-memory table named t. You can then do a select on this table. The second is a "functional form" of select i.e. an alternative syntax for select with extended capabilities. It is an advanced feature that is rarely used, but it's there when you need it "for programmatically-generated queries, such as when column names are dynamically produced". Written in the usual syntax this particular expression is the same as "select from t where c2>35,c1 in `b`c".
I can confirm that in Isabelle/ZF one can set up a context (locale) with the meaning of the ℕ ℤ ℝ ℂ symbols defined so that ℕ ⊂ ℤ ⊂ ℝ ⊂ ℂ. However ℕ for example will not be equal in such case to the canonical set of ZF natural numbers where 1 = {0}, 2 = {0,1} etc.
Isabelle is generic and supports many object logics, listed in [1]. Isabelle/HOL is most popular, but Isabelle/ZF is also shipped in the distribution bundle for people who prefer set theory (like myself).
The NSA publication [Solving the ENIGMA: History of the Cryptanalytic Bombe](https://media.defense.gov/2022/Sep/29/2003087366/-1/-1/0/SOL...) is the best written account of the history of breaking ENIGMA I know about.
Another aspect of this is the readability of the resulting text. The role of a proof in mathematics is not only to certify that an assertion is true, but also to communicate to mathematicians why it is true. Lean and Coq verification scripts are not readable in this sense. They do certify that assertions of theorems are true and (at the current state of technology) that the author of the script most likely knows why they are true, but it is close to impossible for a reader to see what is going on in the proof without running the script step by step in software. The Mizar proof language and Isabelle/Isar were designed to communicate as well and proofs written in those languages can be read and understood directly by humans. For a comparison how the same proof of a simple theorem looks like in Lean, Isabelle/HOL, Isabelle/ZF and Mizar see [1], [2] and [3].
[1] https://lawrencecpaulson.github.io/2024/02/28/Gowers_bijecti...
[2] https://isarmathlib.org/func1.html#a_bij_def_alt
[3] https://mizar.uwb.edu.pl/forum/archive/2403/msg00001.html
Seems that the title of the article has it backwards. From the original paper [1]:
"mitochondrial divergence values between H. diadema samples from the Solomon Islands and New Guinea were greater than any observed divergence values between H. diadema and H. dinops samples from within the Solomon Islands"
The paper describes an example of parallel evolution. There is one species of smaller bats (H.dinops) and then on different islands larger ones evolved from it independently. The bigger bats have all been called H. diadema as they look very similar. So the situation is more like "same size, different species" than what the title suggests.
[1] [Parallel evolution in an island archipelago ...](https://academic.oup.com/evolut/advance-article/doi/10.1093/...)
Or maybe they showed up 200 years ago and thought: this is a very nice planet, except it's a bit too cold. What can we (compel the natives to) do to make it some 6 degrees warmer on average so that it is perfect for us? And the rest is history.
the Roman Empire lasted about 200 years.
The Roman Empire lasted about 500 years - from 31 BC to the fall of the Western Roman Empire in 476. If we include the period of existence of the Eastern Roman Empire it would be almost 1500 years - until the fall of Constantinople in 1453.
Validity of that explanation depends of course on the actual acceleration of the UAP. A human can survive 9-10 g of lateral or front to back acceleration (and less in other directions). Beyond 20-30g there is no way to preserve structural integrity of a human made craft as far as we know. If measurement from both visual and radar data gives more than a 100g then we can claim that the object is not a droid.
In Poland there is no checkbox on a tax forms
Yes, there is, in 2022 it was in PIT 38, sec. E. You need to report purchases even when you have not sold anything as this entitles you to subtract cost when you sell later.
It was a similar experience for me when I tried to learn proving with Isabelle/HOL without an expert help. I gave up and switched to Isabelle/ZF and that was easy, my standard mathematics background was sufficient. I use a subset of the Isar language that is needed for my formalized mathematics hobby (shameless plug: isarmathlib.org). Of course if your goal is software verification, then Isabelle/HOL is the way to go. Btw, Isabelle is not "the HOL based theorem prover", Isabelle/HOL is just its most popular logic.
Having worked with a proof assistant is what separates you from Granville (the interviewee in the article). If he had formalized at least a couple of proofs he would not have written things like "people who convert the proof into inputs for Lean". One does not "convert the proof into inputs for Lean" for a simple reason that a proof written in a formal proof language usually contains much more information than the informal prototype. At best one can try to express similar ideas, but it is far from converting a proof from one form to another. If he had formalized a couple of hundred he would have gained a different opinion on the quality of informal proofs as well. A nice list of typical mistakes can be found in this [answer](https://mathoverflow.net/a/291351/163434) to a MathOverflow question.
To estimate the cost and practicality, assume you build a tower 120 meters tall and machinery able to lift 60 tons block of concrete to the top, then retrieve the stored energy by lowering it to the ground level. Think for a moment how much that would cost. Then calculate: mgh = 60000kg x 120m x 10m/s^2 (assume acceleration of gravity is 10m/s^2 for simplicity, no energy losses due to friction etc). The result is 72 million joules. That is 20 kilowatt-hours, about two days of a single household electricity usage.
Right. Specifically, the codomain needs to be an abelian group. And even that is not sufficient as one needs also an action of the field of scalars on that codomain with the right properties.