Viewing profile — foooobar

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…

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 t…

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 re…

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-communit…

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…

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 wa…

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 …

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 ge…

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 alre…

Buzzard asked Wiles himself, who stated "that he would not want to sit an exam on the proof of Langlands–Tunnell".