Viewing profile — digama0

Fun fact, there have been 3 soundness bugs in lean 4 so far. (They were all fixed within hours.) I expect we have not yet found them all, but I also do not sleep poorly worried tha…

Should I introduce you to https://arxiv.org/abs/2403.14064 ?

If this is your situation, you should absolutely be asking more questions on Zulip. It is really easy to get guidance on how to use mathlib, what things exist and where they are. T…

No, Lean is not suitable for axiomatic investigations, it comes with too much baggage from "classical foundations". As Randall said above, Lean is axiomatically much stronger than …

> Speaking of Miri, is the long term goal to say for certain whether or not a program execution encountered UB? (Which is, of course, different than verifying it before execution a…

Yes, that is incorrect. If you write `partial def foo : Nat := foo + 1` it will be accepted, but `def foo : Nat := foo + 1` is not. So while lean checks that functions terminate by…

The jargon is a bit confusing sometimes. In Lean, "refl" does a whole lot more than prove x=x. It is of course available if you want to prove x=x, but the real power of "refl" is t…

> implementation in C++ rather than a nice functional language for dogfooding To be fair, the main author of Lean has been cloistered for two years writing the next version, Lean 4…

For those who are more into watching talks on YouTube than reading papers, and are interested in the low level hardware formalization aspect of this project, there is a recording o…

The fast proof checker I talk about is mm0-c: https://github.com/digama0/mm0/tree/master/mm0-c . It is (deliberately) bare bones, and I'm planning on formalizing approximately the …

It does, but only if you state the theorem in a particular way. Let's say that you have a verifier A, that checks theorems in Peano Arithmetic (PA). Inside that logic, you can defi…

(I'm the author of the paper BTW.) Regarding TLA+ and CakeML: TLA+ seems like a good idea, Leslie Lamport talks a lot of sense in most of his papers. I especially recommend "Compos…

Metamath has tactics, but they aren't part of metamath per se; they are part of the tools that you use to write proofs. You don't make the rest of the world run the same proof sear…

Software gets more complicated, and so bugs become more common. Hardware gets faster, so speed pressures are reduced on software, so it gets more layered and hence slower; and also…

What if your brain is the bottleneck?

It goes without saying that metamath is not designed to be read from the source directly. To be perfectly fair, Coq isn't either; you can kind of get the gist but to really underst…

The verification of entire proof libraries (like the entire Coq standard library, or the Isabelle Archive of Formal proofs) usually ranges from hours to days, as do some of the lar…

Actually if you use the smm verifier that's been cut down to about 800ms. :) However, most of the theorem provers of today have been built on the philosophy that performance doesn'…

Note that this is editorial license on the part of the writer; Buzzard is proposing the use of interactive theorem provers, which only use a small amount of 80's style AI (backtrac…

Luckily, this is a solvable problem. A theorem prover is software, so you can apply formal methods to it, and prove that the software performs its stated function. The CakeML proje…

Only if you're an ideal rational agent. Maths is hard.

The naming system is pretty compact but also very standardized and reliable, which is important when organizing more than 10000 theorems. That one breaks down as "re + add + cl + i…

If you ever use another proof assistant, you will find that too much documentation is much better than not enough. You can certainly skip the documentation in the main pages if you…

It sounds like you are talking about Cantor's theorem, and its proof is here -> http://us.metamath.org/mpeuni/canth.html . The formalization is both short and straightforward, so w…