deadbeef57

8 ms·

31.
by deadbeef57 5y ago
I think that right now it is not clear why condensed/liquid mathematics would be useful for PDEs. On the other hand, your question > Or does it "contain" topology in some sense, allowing people to continue working with not
32.
by deadbeef57 5y ago
See https://www.math.columbia.edu/~woit/wordpress/?p=10560 , which links to a technical write-up by Scholze and Stix about what they think is the issue with Mochizuki's proof. Woit's blogpost also gives a
33.
by deadbeef57 5y ago
> Lean does not escape this limitation, as it defines the equality type inductively as in Coq. Rather, in a mastermind PR campaign, they successfully convinced non-experts of type theory that they could give them quotient types without b
34.
by deadbeef57 5y ago
Yes and no. If you want to port large low-level proof objects in all their gory detail, then this has been done already. But if you want to port the more concise higher-level proof scripts you run in all the same issues as with regular tran
35.
by deadbeef57 5y ago
As explained in another comment, there is only very mild proof automation going on in this Lean project. Every non-trivial idea has to be supplied to the computer by a human being. The whole circus around Mochizuki's proof of the abc c
36.
by deadbeef57 5y ago
Ok, no worries. I understand that from a theoretical point it's not so nice that defeq is not decidable. But frankly I don't care. Because in practice, I don't know of any example where someone was bitten by this. It only sho
37.
by deadbeef57 5y ago
See also [1] for a follow-up blogpost that is less technical. [1]: https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-...
38.
by deadbeef57 5y ago
The claim that Lean's core is not completely sound is FUD. Completely bogus. You might be confused by the fact that Lean's definitional equality is not decidable, but that doesn't mean it isn't sound. Nobody has ever fou
39.
by deadbeef57 5y ago
So you say that the computer verified proofs of the incompleteness theorem of verifying the wrong theorem? Because there can't be bugs in a computer verified proof. (Of course there can theoretically be bugs in a computer verified pr
40.
by deadbeef57 5y ago
I know of several computer verified proofs of the incompleteness theorem. See entry 6 of https://www.cs.ru.nl/~freek/100/ for a small catalogue. How does this relate to your objection? Are there bugs in the verifi