robinzfc

6 ms·

1.
by robinzfc 12d ago
There are a couple of proof languages that are designed for formalized mathematics (rather than formal verification of software) and to be readable by mathematicians. For example, look at the proof that square root of 2 is not rational writ
2.
by robinzfc 2mo ago
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] https://reference-global.com/issue&#x2F
3.
by robinzfc 7mo ago
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
4.
by robinzfc 9mo ago
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.
5.
by robinzfc 10mo ago
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.
6.
by robinzfc 10mo ago
It's about surreal numbers https://en.wikipedia.org/wiki/Surreal_number
7.
by robinzfc 10mo ago
There are "1498 articles written by 278 authors and 73460 theorems, 14291 definitions" at http://mmlquery.mizar.org/
8.
by robinzfc 11mo ago
> 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-d
9.
by robinzfc 11mo ago
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...
10.
by robinzfc 1y ago
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
11.
by robinzfc 2y ago
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 ma
12.
by robinzfc 2y ago
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 typ
13.
by robinzfc 2y ago
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
14.
by robinzfc 2y ago
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 resu
15.
by robinzfc 2y ago
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?".
16.
by robinzfc 2y ago
A bit of history: Sledgehammer became fully operational in 2007, extended to call external SMT solvers in 2008. Looks like Lean is catching up.
17.
by robinzfc 2y ago
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 .
18.
by robinzfc 2y ago
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 capabil
19.
by robinzfc 2y ago
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
20.
by robinzfc 2y ago
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). [1] https://is
21.
by robinzfc 2y ago
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
22.
by robinzfc 2y ago
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 scri
23.
by robinzfc 2y ago
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 bet
24.
by robinzfc 3y ago
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
25.
by robinzfc 3y ago
> 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 yea
26.
by robinzfc 3y ago
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 i
27.
by robinzfc 3y ago
> 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.
28.
by robinzfc 3y ago
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
29.
by robinzfc 3y ago
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 input
30.
by robinzfc 3y ago
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

More ›