Univalent Foundations: “No Comment.”
mathematicswithoutapologies.wordpress.com
mathematicswithoutapologies.wordpress.com
> some day we may actually write our papers… in language that some smart software could convert into a formal language
What I find fascinating about proof assistants and type theory is what I find fascinating about programming languages in general: they give me a language—and with that a whole world—that is more accessible and manipulable than the less concrete way of thinking so many others seem to prefer. It's like the difference between making something out of Lego as opposed to clay. I'm still making castles in the clouds, but they really exist in a surprisingly concrete way because they're made up of concrete parts. I can feed them into a compiler and execute them or run them through static analysis and answer questions about them… (As an aside, I find the same value in music theory: it provides components needed to turn arbitrary sounds into music without being overwhelmed.)
As a bonus, programs end up inherently well-founded and checked for correctness, potentially to an extent unrivaled by even the most rigorous natural language arguments. But that's just that: a bonus. The real value of a proof assistant is for assistance, not proof. (Which, I should add, is radically different from automatic theorem provers, which are far more relevant for CS than math.)
The lock-in comment at the end is interesting, but not limited to technical lock-in. Mathematics, as a community, already has quite extensive social lock-in—in large part simply because it is a community. And what happens to people whose ideas cannot be expressed in light of this social lock-in (but may, in fact, be entirely consistent)? They are indeed "forced to resort to samizdat, or even blogs, to get their work published". I suppose in a world with finite resources and attention this is inevitable, but I don't think the technical factor changes anything meaningfully. If anything, it's a better sort of lock-in because it would have a technical component independent of social issues, personalities and fashion.
What Lurie seems to be missing is you don't necessarily go "down to the metal" when using an ideal proof assistant. Ideally you should be able to specify almost the same arguments for formalization.
The only fundamental impediment I can think of relates to the following: is there some clear step that (for example) shows a proposition, which might be laborious and hence omitted normally, and is not amenable to being automatically filled in? I'm not sure of the commonality of this case, since as far as I know mathematicians tend to want to minimize intuitive leaps that are not completely obvious.
Even then, it might be useful for all other instances. So how close are we really to getting this piece of software? Seems quite revolutionary for writing mathematics; and equally interesting are the advances required to get there.
Automation works well for first-order logics, whilst proof assistants work with higher-order logics. One consequence is that inductive proofs are very difficult to automate; we can say "XYZ follows by induction", but the computer's often unable to construct such a proof.
There are various approaches to converting back-and-forth between different logics, eg. Isabelle's "Sledgehammer" tool, but
- Some structure can be lost or obscured in the initial translation, which makes finding a proof harder
- Using proofs converted from another logic can cause proofs to be overly-complicated and "unnatural". If they have any computational content (eg. where the proof is a datastructure or function), this can make working with such values more difficult (eg. if we want to prove a property holds in every branch of a function, having an overly-complicated function which branches based on not-completely-relevant conditions makes our life harder).
Deleted comment