In Mathematics, Mistakes Aren’t What They Used to Be
nautil.us
nautil.us
You can just understand proof assistants as an effort to design a language for mathematical proofs, and a procedure to verify them mechanically. (Spelled out like this, it sounds a lot like Hilbert's program -- we have just understood since then that you cannot hope to have a "perfect" proof assistant.) The availability of computers means that you can actually implement the verification process and run it, but if you do not want to involve computers in the process (because you do not "trust" them, or whatever), you could always check such proofs by hand, in principle.
In a sense, a proof designed for a computer assistant is one that can be verified without any intelligence required from the reader.
> Voevodsky himself is careful to distinguish the various ways computers should or shouldn’t be put to use. “Lots of people don’t understand the difference between using computers for calculation, for computer-generated proofs, and for computer-assisted proofs,” he says. “The computer-generated proofs are the proofs which teach us very little. And there is a correct perception that if we go toward computer-generated proofs then we lose all the good that there is in mathematics—mathematics as a spiritual discipline, mathematics as something which helps to form a pure mind.”
[1] https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimi...
Apart from Voevodsky's work, there are several other big math formalization projects. Perhaps the biggest ones are the formalization of the Feit-Thompson theorem (done by Georges Gonthier and his collaborators, in Coq), and the proof of the Kepler conjecture (done by Thomas Hales and his collaborators, in Isabelle/HOL and HOL Light).
On the other hand, many of his collaborators are interested in the project precisely because it uses Coq and they like constructive mathematics. So the HoTT book only uses exluded middle when necessary (and carefully tracks where), and developing a computational interpretation of univalence is considered to be an important task.
Edit to add: So why would someone who doesn't care about constructivism want to use Coq? Because it's based around typed objects. Apparently, homotopy theorists had for a long time been aware that instead of basing mathematics on sets, and then constructing equivalence classes on top of those, you could take homotopy types as primitive.. something like basing mathematics on blobs rather than points. This was all considered theoretical and impractical--until someone noticed that the logic provided by Intensional Type Theory (as implemented in e.g. Coq) can be considered to do exactly this!
http://en.wikipedia.org/wiki/Homotopy_type_theory#Univalence...
I am hazy on the details, but I think TLA+ proofs are just checked by brute force, and not with an actual theorem prover? It's for distributed algorithms with a large but finite number of states.
So it's not exactly the same as what's discussed in the article, but it's definitely related. I would appreciate if anyone has any clarification on this point.
https://scholar.google.com/scholar?cluster=14553320809011812...
"A method of writing proofs is described that makes it harder to prove things that are not true. The method, based on hierarchical structuring, is simple and practical. The author's twenty years of experience writing such proofs is discussed."
http://research.microsoft.com/en-us/um/people/lamport/pubs/p...
TLA+ is sufficiently different from Coq -- and in ways essential to Voevodsky's intentions -- that discussion of TLA+ in this article would be out of place.
In addition, there is a huge community of people who have worked with theorem provers for the past 20 years or more; it's not clear to me why the author would single out TLA+/Lamport over any of these other systems/researchers.
If it were a technical journal, maybe they wouldn't be related. But they're definitely related for a popular article.
Hence my last paragraph -- they're only related in the sense that the entire formal methods/verification/theorem proving community is related. Given the hundreds of systems/researchers that would make for interesting additions to the story, it's not surprising that TLA+ isn't mentioned.
(Incidentally, the author's choice representative for "other people are doing this too" -- Automath -- is probably just as good of a choice as TLA+.)
To give an elementary example, you can conjecture that a given mapping is something-morphism between two groups and use that morphism to carry out a proof about one group in terms of a known result about the other group.
In fact, "conjecture lemma; verify main result is true using the conjectured lemma; go back an prove lemma" is a bog standard problem solving technique in Mathematics...
edit: Oh, I see what you mean is bit more nuanced than I understood at first. But this is still true -- often you can probably check that the mapping you've written down is a something-morphism locally, for the elements you're working with atm. I'm stretching the example now, but you get my point? I imagine this is probably not unheard of in research-grade mathematics -- e.g. we don't have a general proof for "really cool conjecture" so we check it in special cases whereever we think it might be useful to have... idk.
http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundation...
https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimi...
What's not to love about:
The univalence axiom states:
(A = B) ≃ (A ≃ B)
"In other words, identity is equivalent to equivalence. In particular, one may say that 'equivalent types are identical'."
I wish I knew enough about functional languages to ask the same question there.
Equality is already a very overloaded term in mathematics, but roughly means "these are the same thing" - X^2 is 'equal to' X * X for example, or in most cases we think simply of the identity relation on some set or whatever. Isomorphism states that two things can be 'transformed' into each other through the existence of a function, along with its inverse.
For example, the sets {A, B, C} and {1, 2, 3} are not equal, but isomorphic because you can define a bijection between them: A = 1, B = 2, C = 3. In some sense equality is 'more rigid' than an isomorphism, obviously. Also, you have to choose the bijection explicitly here because in this case, more than 1 valid one exists, which is another aspect of an isomorphisms 'identity'.
The univalence axiom states that in this new constructive mathematical framework, 'equality' and 'isomorphism' are exactly the same thing.
I suppose in some sense you can view concepts like "object identity" and "object state" in some languages like Java in the same bucket, because while two Java objects may be "equal in terms of state" (members all the same) they might not be "equal in terms of identity" (because they point to different heap objects).
But this kind of distinction mostly doesn't make sense in functional programming languages because you often throw the notion of 'value identity' out the window, so 'equality' in these languages is defined solely as mathematical equality - that we can 'normalize' two expressions to the same final form. 'isomorphism' then, normally just has an interpretation like two functions `a -> b` and its inverse `b -> a`, so even in these languages, we aren't quite talking about the same things.
HoTT is much more radical than all of this when you look at it together of course - because it's more like saying if you have two proofs that x = y, you can think of 'x' and 'y' as points in space, and proof of equality is a path from x to y in this space - so two proofs of equality are just two distinct paths.
The 'space' on which these points exist is actually not sets but 'types', which is like a set, but also including propositions too. So now the set 'X' and propositions about X exist together. Proving some proposition requires 'constructing' a value of that propositions' type, using the elements and propositions already existing. In a language like Haskell, to implement a function of type 'f :: A -> B' requires being able to 'construct' a B given a value of type A - to do this, in effect, is a proof that 'A -> B' does in fact exist, because you built it.
Also, under this interpretation of 'space', which is topological, equivalent paths give rise to notions of 'homotopy' (saying a path A can be 'morphed into' a path B), so if you have two 'paths' representing the proofs of x = y, these 'paths' admit a homotopy between them. And furthermore you can have notions of homotopies between homotopies, etc etc. So things get very 'higher order'. Types can also be viewed as an 'infinity groupoid', which is a thing that not only has elements and isomorphisms between elements, but isomorphisms between isomorphisms, and isomorphisms between those, infinitely. So if you squint you can see how this infinity-groupoid notion of 'higher order' isomorphisms between other isomorphisms, and higher order homotopies, are all very closely linked. It's all very strange and unifying and delightful.
That's the extremely handwavy explanation that is might be pretty fluffy, but it might help.
"When is one thing equal to some other thing", by Mazur
When people emphasise intuition in mathematics it suggests that
(i) that they have never tried to teach mathematics formally and explicitly without appeal to intuition —if they had, it would have been a most refreshing experience for them and for those of their students that were sufficiently well-educated to appreciate simplification
(ii) that they have never taken the trouble to learn how to let the rules of the formal game guide their “writing of papers” —if they had, they would have discovered how to do mathematics way beyond their former powers.
EW Dijkstra
Given all that I think the Oxford dictionary's definition is actually quite spot on. Are you quibbling with it? Happy to hear what you think.
I can post links to Brouwer's writing on these matters.
[0] This word causes other issues, but the, ha, intuition of it is not so bad
A nice overview was given by Peter of Conscious Entities recently: http://www.consciousentities.com/?p=1918.
This isn't a particularly strong argument, as solutions verified via the informal communication method of 'speech' often pass verification without being correct.
This is unclear. Do you mean that computers can't solve the Halting Problem, but humans can solve many instances of the question "will this question halt"? Then you're not comparing apples with apples. You should instead compare human reasoning of "this program will halt or not" with programs developed in the field of termination analysis. Are these analysis bad compared to human ones?
Or do you mean that humans can prove the undecidability of the Halting Problem, but computers can't manage to prove or disprove it, or understand the human proofs? Does this have to do with such proofs tend to be non-constructive, as far as I've seen?
In any case, I guess it's still an open problem whether or not the human mind can algorithmically solve the Halting Problem, right? Our minds would have to be "better" than a TM.
Funnily enough, I was just thinking about this very topic a week ago and scribbled down some notes with slightly less trivial examples: http://www.maths.tcd.ie/~onash/counting_whats_important_file...
I like point (ii) above, as learning to let the rules of the game guide your writing is a very powerful technique indeed. But teaching math formally without appeal to intuition is what a lot of people do and it's boring and unpleasant to me. It doesn't simplify, it merely traces lines in the sand or on a page without taking the trouble to look up and appreciate the larger picture (sometimes meaning literal picture).
It's clear that Dijkstra & I appreciate very different parts of mathematics :)
The Homotopy Type Theory (HoTT) book[1] puts forth a possible interpretation of Conway's thoughts about univalent foundations in section 11.6 (look at the bottom of the page for the following very selective and paraphrased quote):
"[...] Conway's point was not to complain about ZF in particular, but to argue against all foundational theories at once [...] One might respond that, in fact, univalent foundations is not one of the "standard foundational theories" which Conway had in mind, but rather the metatheory in which we may express our ability to create new theories, and about which we may prove Conway's metatheorem."[2]
[1] http://homotopytypetheory.org/book/
[2] http://www.math.ntnu.no/~stacey/documents/HoTT-online/main12...
EDIT: I forgot to mention that Voevodsky's definition of "Univalent Foundations" seems to be used interchangeably with the term "Homotopy Type Theory", but in Voevodsky's mind there is a sharp distinction[3]. Voevodsky tried to make this clear in an HoTT Google Groups email thread with the following statement: "HoTT is the study of the type-theoretic approach to the meta-theory of the Univalent Foundations."[4]
[3] http://en.wikipedia.org/wiki/Homotopy_type_theory#Univalent_...
[4] https://groups.google.com/forum/#!topic/homotopytypetheory/z...
Basically, humans can't comprehend what the computers are doing, even when they are right, and we aren't always building them well enough to be trustworthy without checking their work.
However, Zeilberger and Shalosh B Ekhad have done some highly reputable work, albeit in a narrow area. (Zeilberger designs algorithms in combinatorics, which then computer-generate proofs for specific questions)
http://www.nytimes.com/learning/teachers/featured_articles/2...
Within the formalized version of mathematics, some sort of namespace mechanism will probably be necessary to deal with terminology collisions.
And certain things commonly thought of as one notion might need to be split up into multiple notions (example: in some contexts, "function" means "set of pairs satisfying the vertical line test"; in other contexts, "function" means "set of pairs satisfying vertical line test, along with designated 'codomain').
But at most, this amounts to changing the wallpaper. The structure itself is sound unless something really shocking happens like a proof that PA is inconsistent or something. Such a shocking event needn't hinge on computer-aided proofs (although computer-aided proofs will surely help to convince mathematicians who would otherwise assume such a startling result must be mistaken).
The critical parts in mathematics are the foundations and basics. These have been studied over and over again by many smart people. I think if there is something wrong, it would have been found. If you are familiar with mathematics you will probably agree with this assessment.
And, in the unlikely case that there is an issue, then it will be worked around, so no harm is done to the rest of mathematics. Luckily, in mathematics, we make the world (axioms and definitons) like we wish it to be. There is a famous quote I don't recall right now about mathematics being now in the garden of eden and mathematics shall never be forced to leave it again.
However, non-critical parts of mathematics like advanced research is often plagued by mistakes.
Computer-verified proofs are the necessary future of mathematics.
One little remark, people often assign more attributes to functions than just the mapping-tuples itself and optionally the codomain. Often the arithmetic formulation of the mapping is part of the function because we want to differentiate based on the way the function is written.