Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

Possibly this? http://www.macs.hw.ac.uk/~ek19/ML4PG/ It's mostly in maintenance mode (at least, I seem to have inherited its maintenance; and it's such a horrible mess of Emacs Lisp + Matlab + shell scripts that I don't dare touch it unless asked ;) ).

It's used for clustering statements and proofs, the idea being that if you're stuck trying to prove something, you might be able to find something "similar" in an existing library to use as inspiration. It's mostly to help with manual searches, rather than automatically solving anything (although there is some related work on doing that for Coq called SEPIA https://arxiv.org/abs/1505.07987 and ACL2 http://www.macs.hw.ac.uk/~ek19/ACL2ml/index.html ).

> The painful part is that you're using tools which are trying to bridge between wildly different logical foundations.

If you're referring to the fact that many proof assistants (e.g. Coq) are based on constructive/intuitionistic type theory, whilst most mathematics is formulated in classical set theory, then yes there is some translation involved. However, I would point out that we can use classical logic pretty easily by adding excluded middle, double negation elimination, etc. to an intuitionistic system (this is available in the Coq standard library https://coq.inria.fr/library/Coq.Logic.ClassicalFacts.html ). There are also systems which can use set theory (directly or indirectly), like Metamath and Isabelle.

Personally, I much prefer type theory (which I self-learned, before pursuing a related PhD) to set theory (which I was taught as an undergraduate and enjoyed, but not enough to do it as a hobby). However, I'm well aware that my computer scientist background is nothing like that of a trained mathematician.

I'm inclined to agree with you; though the key word here is "trivial".

Types are propositions, and programs are proofs of their types. Unfortunately most programs are overly-complicated proofs of trivial propositions (when looked at from the mathematical side of curry-howard; of course what's actually the case is that we tend to only use types to specify a tiny part of what our programs are meant to do).

In an untyped language every expression has the same type (which we might call `Thing`, and contains integers, strings, functions, etc.) so in the curry-howard sense every expression is proof of the same trivial proposition.

I'm inclined to think of the laws of physics (whatever they are) as a programming language, and physical systems as programs running in that language. On first impression, it doesn't seem like physics is typed; hence every physical system is a proof of a trivial proposition (essentially: physical things can exist). It would be interesting to hear a counterargument though.

Note that in these cases it's the types/propositions which are trivial, not necessarily the programs/proofs. Consider that we could, if we wanted, prove a pretty trivial proposition like `((A -> B) AND A) -> B` in a roundabout way that involved applications of Fermat's last theorem. I tend to call such things "(over)complicated", rather than "complext", since their complexity isn't inherent or required.

It's not so much that programs are isomorphic to proofs; it's that mathematics and programming are the same activity. It's essentially a historical accident that the people who practice this activity have ended up in different groups, and that those groups use different terminology for the same things ("program" vs "proof", "type" vs "proposition", "execute" vs "simplify", "tuple" vs "conjunction", "union" vs "disjunction", "function" vs "implication", "dependent function" vs "universal quantification", "interface" vs "existential", "programming language" vs "logical system", etc.).

All of the relationships between these are the same too (e.g. a program `p` has type `T`, iff the proof `p` proves the proposition `T`; the proof `w` proves that the existence of `x` implies the proposition `y AND z` iff the program `w` is a function which generates a tuple of `(y, z)` when given an argument implementing the interface `x`; and so on).

Mathematicians and programmers do care about different things. Mathematicians are more concerned with informally proving previously unknown results; which corresponds to something like learning that a type has a value by sketching some pseudocode. Programmers care deeply about how many steps their proofs (programs) take to simplify; how easy it is to modify a proof to prove a slightly different proposition, etc. Yet there are so many good ideas on each side that are immediately applicable (e.g. dependently typed languages take rigorous logical systems and view them as programming languages; proof engineering takes software engineering ideas and applies them to building and maintaining proofs).

I'm struggling to think of an activity involving rock gardens that corresponds precisely to, say, universal quantification.

I think you are exaggerating the difficulty of theorem statement compared to proof. Here is one (admittedly extreme) example in Lean, from the formal abstracts website.

theorem Wiles_Taylor : ∀ (x y z n : nat), x > 0 → y > 0 → n > 2 → x ^ n + y ^ n ≠ z ^ n := more years than I have to spare