robinzfc
No user record in our sample, but robinzfc has activity below (stories or comments). Likely we have partial data — the full bulk-load will fill profiles in.
No user record in our sample, but robinzfc has activity below (stories or comments). Likely we have partial data — the full bulk-load will fill profiles in.
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…
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…
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…
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…
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…
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"…
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…
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…
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]…
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…
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…
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?…
> 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…
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…
> 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…