3 ms·

Not a mathematician either, but Tao's view does make sense for me. What Lurie seems to be missing is you don't necessarily go "down to the metal" when using an

Not a mathematician either, but Tao's view does make sense for me. 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.

chriswarbo 11y ago
> 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? 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).

chriswarbo 11y ago

> 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? 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).