foooobar

4 ms·

1.
by foooobar 5y ago
I think Kevin is asserting that to make strong comparative claims about the quality of either system, it's good to have a large and functionally similar body of work to compare the systems with, not that there is no way to improve on L
2.
by foooobar 5y ago
Thanks! But does that not already answer your question as to why Lean would use CIC and not a simpler metatheory? That particular paper is from 2016 and the type theory presented there is still lacking a number of features from CIC, with th
3.
by foooobar 5y ago
What simplifications do you have in mind? I think one of the reasons is that Lean's approximation of defeq still works well enough in practice. As mentioned by others, you never really run into the kind of counter examples that break t
4.
by foooobar 5y ago
If you're interested in interactive theorem proving with Lean (and not condensed mathematics), the Lean community landing page is a good place to start. https://leanprover-community.github.io/ Especially the "Natu
5.
by foooobar 5y ago
Some constructivists may also take offense with proof irrelevance (and the resulting loss of normalization [1] or its incompatibility with HoTT), which you can only really avoid by avoiding Prop. [1] https://arxiv.org/abs&#x
6.
by foooobar 5y ago
I don't think anyone is trying to sell Lean as a constructive system. The current developers certainly don't think of it that way, further evidenced by the fact that the typical way of doing computation in Lean does not involve de
7.
by foooobar 5y ago
As far as I can tell, this is not quite true. Tactic proofs aside, you can also write functional term mode proofs and declarative "structured" proofs in the sense of Isar. Theorem Proving in Lean introduces that style, so most peo
8.
by foooobar 7y ago
Which tutorial did you use? As someone coming from computer science, I found https://leanprover.github.io/theorem_proving_in_lean/ very approachable as an introduction to ITP in general.
9.
by foooobar 7y ago
Because the book is a great introduction to theorem proving in general. All those concepts learned translate nicely to other theorem provers, and especially Lean 4. Lean 4 has already gone public: https://github.com/leanprov
10.
by foooobar 7y ago
Buzzard asked Wiles himself, who stated "that he would not want to sit an exam on the proof of Langlands–Tunnell".