Viewing profile — robinzfc

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). [1…

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] abou…

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…

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 en…

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 ou…

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 ma…

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. Isabell…

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 th…

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 …

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 a…

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 i…

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 s…

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 h…

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 mat…

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 Guin…

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 o…

> 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 existenc…