4 ms·

I found this really worth watching, as much for the sociological commentary about the way modern mathematics is done as for the presentation of the program (and

I found this really worth watching, as much for the sociological commentary about the way modern mathematics is done as for the presentation of the program (and the latter resonates strongly for me). One of the more interesting bits for me was in the Q&A, where Prof Buzzard was asked about alternatives to Lean. Lean is the most evolved of the dependent-typed calculus of constructions provers, but two other approaches might work. One is univalence, which is sexy, but Prof Buzzard observed that they haven't actually got much done in their system. The other is set theory, which is more familiar and approachable to working mathematicians, but the systems out there lack automation. He didn't mention Metamath by name, but that's currently the most developed such system, and they have managed to get a lot done, either in spite of or because of the lack of type theory sexiness of the foundations. So the question I'd love to see answered is whether automation is inherently easier in type theory, or whether it might be possible to build automation for a set theoretical approach. John Harrison gave a talk last year at AITP on the topic, but I haven't heard much more of this.

Miltnoid 7y ago
No way is Lean more evolved than Coq.
- raphlinus 7y ago
  Maybe that wasn't the best way to phrase it, but the question was asked and Prof Buzzard replied basically that in Lean it's straightforward to express quotients, while in Coq you get "setoid hell". This specific statement is at 1:04:20 in the video. The question is at 1:00:02, and is probably useful for context.
  - zozbot234 7y ago
    Aren't quotients non-constructive? Univalence is probably also relevant to this issue, given that it generalizes the treatment of 'equality' in a broadly similar direction to the one needed for quotients. Groupoids are after all a fairly natural generalization of setoids.
    - raphlinus 7y ago
      Quotients are not purely constructive, but they are present in Lean as an extension (this is covered in Chapter 1 of the book[1]). [1]: https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf https://leanprover.github.io/theorem_proving_in_lean/theorem...
      - uryga 7y ago
        could you point me towards an explanation of why quotients aren't constructive?
        ratmice 7y ago
        I can't, perhaps lean's definition of quotient isn't constructive (I hadn't looked or noticed that), But there is at least this construction of quotients in NuPRL. http://www.nuprl.org/documents/Nogin/QuotientTypes_02.pdf http://www.nuprl.org/documents/Nogin/QuotientTypes_02.pdf I think quotients are not typical of constructive objects in that if you construct some object, and then project it into the quotient, then you have the quotient, but you cannot project that object back out. You get subtly less, that the resulting quotient satisfies some equivalence relation. Under a specific set of assumptions, you may very well be able to construct the quotient... but under a different set of assumptions (including the assumption of the quotient), Perhaps in these differing sets of assumptions, you have the quotient, but lack the assumptions necessary to construct it yourself. Anyhow, the argument that they are non-constructive in a humpty dumpty sense you cannot put it together -> take it apart -> put it back together again. Where it seems reasonable to consider the "put it together" phase as not entirely incompatible with constructivity?
        uryga 7y ago
        thanks for the reply! i'm gonna need some time to mull it over... would you be able to say how "normalizing" fits into this? by "normalizing" i mean applying some function that takes each equivalence class to a representative element (think simplifying fractions). using something like that, we could round-trip a value (object -> quotient -> object), though at the end we might end up with a different value than what we put in. so yeah, a normalizing function seems like a useful thing when looking at quotients constructively. sorry for the handwavyness, i hope i managed to get my point across!

Miltnoid 7y ago

No way is Lean more evolved than Coq.

raphlinus 7y ago
Maybe that wasn't the best way to phrase it, but the question was asked and Prof Buzzard replied basically that in Lean it's straightforward to express quotients, while in Coq you get "setoid hell". This specific statement is at 1:04:20 in the video. The question is at 1:00:02, and is probably useful for context.
- zozbot234 7y ago
  Aren't quotients non-constructive? Univalence is probably also relevant to this issue, given that it generalizes the treatment of 'equality' in a broadly similar direction to the one needed for quotients. Groupoids are after all a fairly natural generalization of setoids.
  - raphlinus 7y ago
    Quotients are not purely constructive, but they are present in Lean as an extension (this is covered in Chapter 1 of the book[1]). [1]: https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf https://leanprover.github.io/theorem_proving_in_lean/theorem...
    - uryga 7y ago
      could you point me towards an explanation of why quotients aren't constructive?
      - ratmice 7y ago
        I can't, perhaps lean's definition of quotient isn't constructive (I hadn't looked or noticed that), But there is at least this construction of quotients in NuPRL. http://www.nuprl.org/documents/Nogin/QuotientTypes_02.pdf http://www.nuprl.org/documents/Nogin/QuotientTypes_02.pdf I think quotients are not typical of constructive objects in that if you construct some object, and then project it into the quotient, then you have the quotient, but you cannot project that object back out. You get subtly less, that the resulting quotient satisfies some equivalence relation. Under a specific set of assumptions, you may very well be able to construct the quotient... but under a different set of assumptions (including the assumption of the quotient), Perhaps in these differing sets of assumptions, you have the quotient, but lack the assumptions necessary to construct it yourself. Anyhow, the argument that they are non-constructive in a humpty dumpty sense you cannot put it together -> take it apart -> put it back together again. Where it seems reasonable to consider the "put it together" phase as not entirely incompatible with constructivity?
        uryga 7y ago
        thanks for the reply! i'm gonna need some time to mull it over... would you be able to say how "normalizing" fits into this? by "normalizing" i mean applying some function that takes each equivalence class to a representative element (think simplifying fractions). using something like that, we could round-trip a value (object -> quotient -> object), though at the end we might end up with a different value than what we put in. so yeah, a normalizing function seems like a useful thing when looking at quotients constructively. sorry for the handwavyness, i hope i managed to get my point across!