I wish these attempts were using constructive mathematics but I understand that that would turn away a lot of mathematicians.
In the Lean approach, anything not marked `noncomputable` in the Type universe and above needs to be constructible, in the sense that there is a program that can compute such an object using a functional programming language (where the function is guaranteed to terminate), but proofs don't need to be constructible in the same way. Proofs are still functions, but they're free to use things like the axiom of choice in the course of a proof. The way things are set up, even if you use non-computable things while making your inferences, this "forbidden" data will not leak out.
It seems eminently reasonable to me that you can argue a program computes the correct thing because it doesn't compute the wrong thing, and unless you're specifically studying different toposes/logics, I'm not sure what constructive logic would really give you (and it's not like mathematicians slavishly keep track of where they used the axiom of choice or its consequence the LEM).
How this all looks in Lean practice is that it's stronger to give a definition and prove it satisfies a property than to prove a "there exists" statement. mathlib authors tend to go for the first, unless the result is inherently noncomputable. There's also a facility for lifting propositions up to boolean values, which more or less amounts to giving a constructive proof -- this is used pervasively, for example with finite sets, which are constructive in the sense that if you have one there's an actual finite list backing it.
I guess in short: it's a useful middle ground being able to prove something exists without having to construct it, but if you want to "have" the thing that purportedly exists you need to construct it.
However finite graph theory is not remotely mainstream mathematics. Take your favourite super-prestigious maths prize, for example the Abel Prize or the Fields Medal. Now look at everyone who has won this prize in the last 10 years. That is the definition of mainstream mathematics. And as you will see if you do this, the areas which these people are working on are a million miles away from finite graph theory. This is precisely the problem. Computer scientists sometimes have a very twisted view of exactly what kind of mathematics is regarded as important in 2021. The experiment I outline above will give you some idea of what is mainstream, and believe me, it's not the four colour theorem.
And I say this as someone with no interest in graph theory, or combinatorics in general.
Further, I don't think it is "elite provincialism" to point out this readily verifiable fact. Besides looking at the big prizes, we can look at any of the top journals (Annals, IHES, Inventiones, Journal of the AMS, Acta, whatever). You're not going to find a lot of finite graph theory there.
Now, I think we should separate the question whether it is the case that he's right about what mathematicians value from the question of whether it ought to be the case that the world is this way. As I just said, the answer to the first question is yes. I'd argue that the answer to the second question is also yes, but that's a whole different discussion.
The irony is that I suspect every single mathematician, elite or not, knows what the four-color theorem is, far more than could tell you what chromatic homotopy is, or state anything about the Langlands program beyond "Uh, it's something about number theory? And groups? Maybe?"
Further, it's not like no finite combinatorics/graph theory gets published in these journals. Just not a lot, because it's not sufficiently interesting/valuable to the broader community. (Annals of Math almost published Hales's proof of the Kepler conjecture, after all; eventually a proof appeared in another top journal.)
Also, re: connections, you can easily check the author affiliations for papers in these journals. There are plenty of people from universities that are not so well known. It's hardly an "old boys club."
You can see a letter to the editor of the Bulletin about it. Look at the affiliations of the people protesting the decision, and the affiliations of the editors defending it: http://www.ams.org/notices/200706/tx070600694p.pdf
Again, whether you think the criteria should be the way they are is a separate conversation.
Calling this 'non-classical' is interesting—it's definitely non-classical from the point of view of formalisation, but I'm not sure formalisation has been around long enough to have classics ….
As of course you know but non-mathematicians may not, from a non-formalising mathematician's point of view, it's the non-constructive logic that's classical, to the extent that it's actually sometimes called classical logic (https://en.wikipedia.org/wiki/Classical_logic).
I am working on some hobby projects, similar but very much more elementary to what you are doing. May I please kindly get your e-mail address (or you may drop me a note at ashok dot khanna at hotmail dot com). I would love to connect and follow your work.
I apologise as I was not able to find your e-mail address on your blog post - sorry if I missed it.
Best wishes,
See, that is one of the problems with constructive mathematics. It not only requires you to write down the algorithm, but also to prove it constructively, although a non-constructive proof would be perfectly fine. In other words: constructivism is often overkill.
Let's say you need an algorithm for a real-life situation, and you manage to write one down.
Ok then, you are good to go, just use it!
But ... how do you know that the algorithm you have written down is correct?
Now, a constructive mathematician would require you to also provide a constructive proof for your algorithm. A mainstream mathematician would additionally also be fine with a non-constructive proof for your algorithm. So, who is more real-life?
In general, my hypothesis is that if you restrict yourself to constructive mathematics, you are limiting yourself. And that is true whether your chosen field is algorithms, or not.
Now, if you offer me for a given algorithm a constructive proof, that's great. But if you needed 10 years to give me that proof, and a non-constructive one can be had in 10 minutes, I might not be so enthusiastic if I had to pay your salary, or if I needed that result really urgently, or both. But on the other hand, IBM probably doesn't care.
And you should have seen the answer that I wrote before that, and then deleted. Now THAT answer was impolite. Goodnight to you as well.
> I'm sure they would much prefer that it was constructive, rather than non-constructive
One point against constructivism is that the proof could be less readable.
> can produce a usable algorithm from the constructive proof
No. Between the automated tactics and inductive propositions constructed to carry all kinds of redundant state helpful in proving your properties, your proof objects won't be anywhere near production level. And constructive proof checkers don't intend that to happen anyway: you pretty much define an efficient function in a DSL, then use a different DSL to prove that the function fulfils the properties. The proof object is pretty much a black box with unclear efficiency that wasn't meant for humans to read.
My algorithm: If a + b == c then output 1. If a^2 + b^2 == c^2 then output 2. Stop.
This algorithm is correct, because Fermat's last theorem holds. Now, try to come up with a simpler algorithm than that, and one that in addition has a constructive proof.
And we are done, because the statement of the theorem in the "classical fragment" of constructive logic is identical to the constructive statement as it does not involve any existentials or disjunctions. However if the theorem did involve a limited use of these connectives, we could use Goedel's Dialectica interpretation[3] to turn them in to their constructive counterparts, as long as the theorem is Pi_2 or lower, which is going to be the case for the vast majority of theorems about software.
[1] https://news.ycombinator.com/item?id=26217587
[2] https://en.wikipedia.org/wiki/Absoluteness#Shoenfield%27s_ab...
[3] https://www.andrew.cmu.edu/user/avigad/Papers/dialect.pdf
That is very cool! So, even less reason to demand a constructive proof, a non-constructive one is then often good enough even for hard-core constructivists.
Do you know if this has been implemented in any actual (interactive) theorem proving system, for example Lean? It sounds like a great feature to me to allow non-constructive proofs in certain situations, but to have the theorem hold even in a constructive setting.
Myself, I've never seen an automated theorem prover that will perform this sort of translation automatically. I have, on rare occasion, gone through by hand to remove uses of classical axioms in Coq proofs of theorems than ought not to be using them. Usually the uses are pretty superficial.
And dependent type theory is gleaming when things that normal mathematicians think of as propositions are not only values, but functions! For example a list l1 being a subset of a list l2 is a function from memberships of l1 (which, remember is data) to memberships of l2. Now you get partial evaluation when working on your proofs and things just magically unify.
I write about these examples in experience I had in "Taking Propositions as Types seriously" @ <http://r6.ca/blog/20171008T222703Z.html>.
There is a practical difference between Principia Mathematica taking 370 pages to prove 1 + 1 = 2 versus dependent type theory's proof `refl_equal 2`. (I'm exaggerating, but only a little).
But yes, being able to work with functions as data is also very important! That's why I am pursuing a combination of simple type theory and set theory as the foundation of a theorem prover, as I have outlined here: http://www.practal.com
Similarly, all classical uses of LEM (A ∨ B) can be understood as constructive statements of the form ¬(¬A ∧ ¬B).
Here is the reason why it's obvious for mathematicians. If you're trying to prove a theorem (e.g. the theorem that class numbers of imaginary quadratic fields tend to infinity), and then someone comes up with a proof which assumes that a certain generalisation of the Riemann hypothesis is true, and then someone else comes up with a proof which assumes that the exact same generalisation is false, then we mathematicians say "great, the theorem is now proved". This actually happened.
However if your boss asks you to write some code which does a calculation, and the next day you show up in their office with two USB sticks and say "this code is guaranteed to produce the correct answer if the Riemann hypothesis is true, and this other code is guaranteed to produce the correct answer if the Riemann hypothesis is false" then you are going to lose your job, because all you did was prove that the code exists, which is less helpful than it could be.
For me one of the biggest problems with the area of formalisation of mathematics is that for decades it has been dominated by computer scientists, whose view of what is important and beautiful in mathematics does not really coincide with that of the working mathematician. This is what I am fighting to change.
Oh wow! Was it an interesting theorem that got proved this way? Did it get proved in another, less controversial manner as well? Could you provide a pointer to it?
In Kevin's example where you have two programs, one which depends on the Riemann hypothesis being true and the other which depends on it being false, is that you can't just execute the programs -- they might have undefined behavior since they depend on the truth of some statement during their executions, and there's no general algorithm to decide whether undefined behavior is happening. They depend on undecided facts, so you can't put them together into a single program that decides the result. (Maybe a slogan is "truth can be contingent, but data cannot be.")
In Lean syntax, this is an example type signature of something that takes two programs (h and h') that respectively take in the truth/proof of a proposition or its negation, along with a proof that there is at most one element of α, and produces that element. I don't think there's a way to write this definition in Lean without marking the definition noncomputable:
def extract {p : Prop} {α : Type*}
(h : p → α) (h' : ¬p → α)
(unique : ∀ (x y : α), x = y) : α := sorry
That’s where opinions will differ. That’s only true if you accept the law of the excluded middle.
Mainstream math does, but most constructive math does not.
Yes, Kripke semantics makes sense of constructive logic. Topos theory, too. But I really think of all of these embedded in classical logic, and assuming that the law of excluded middle doesn't hold for general reasoning just doesn't make any kind of sense to me.
p.s. could you let me know your e-mail so I can keep for future reference, as I'm also working on a hobby project for automated theorem solving.
If you assume P, derive a contradiction, then conclude not P, that is a direct proof of negation not a proof by contradiction.
In a non-constructive mathematics it is true that 'either A or not A is true' and that allows you to prove existence of objects with certain properties by disproving their non-existence (if it cannot not-exist then it has to exist, by the law of excluded middle). Constructive mathematics, on the other hand, says that that's not enough and to prove that there exist objects with some properties you have to prove their existence.
The way I understand it is that if you have the law of excluded middle you cannot discard 'non-constructive' proofs as invalid since they follow straight from the axioms.
“reject” would mean that if, given their set of axioms, it could be proven, they would try and tweak their axioms in order to make it unprovable or provably false in their system (“we think this cannot and should not be true”)
So, “not reject” means they would happily use it in their proofs, if it could be proven from their set of axioms (“interesting. That gives us a powerful tool to do proofs”)
So we can't claim constructive mathematicians reject excluded middle, since they reject the rejection of excluded middle. I admit this will be confusing for people used to classical logic at first, even those for whom English is their native language.
> The way I understand it is that if you have the law of excluded middle you cannot discard 'non-constructive' proofs as invalid since they follow straight from the axioms.
This is accurate, my above point is just a pedantic one about semantics.
If you are familiar with "Classical" logic, constructive math omits the law of excluded middle (e.g. "A or not A" must be true). In ZFC, the axiom of choice is omitted.
This leads to proofs that are not only a verification of some idea but also gives you the mechanism to compute the evidence. This is often described as "the computational content of proofs" and is especially valuable in the context of the Curry-Howard isomorphism: for every proof, there is a corresponding program (and vice-versa). This is the basis for formal verification of constructive proofs. When creating a proof in Coq, you are actually writing the corresponding program. And you can even extract the program in another general purpose programming language (usually OCaml in the context of Coq, but Haskell is also supported).
The constructive logic used in constructive mathematics is classical logic with two new connectives added: the constructive existential, and the constructive disjunction (which could be defined in terms of the constructive existential).
The constructive disjunction and constructive existential connective has semantics given by the BKH interpretation[1]. A proof of the constructive disjunction A + B is either a proof of A or a proof of B. A proof of the constructive existential Σn:N. P(n) is a pair <n,p> where n is a natural number and p is a proof of P(n).
So constructive mathematics isn't classical mathematics hindered, but constructive mathematics is mathematics enhanced with a more expressive language. Naturally constructive mathematics tends to focus on theorems written in this more expressive language that make use of these new constructive connectives, rather than focusing on the classical fragment which is already well studied.
For the non-layman: we can see that the above interpretation is correct because the fundamental logical rules for universal quantification, implication, conjunction, false and true are all identical between classical and constructive logic. And, according to classical mathematicians at least, this set of logical combinatorics is complete. Thus the law of excluded middle holds, even in constructive logic, so long as you use the classical disjunction, which is defined in terms of conjunction, implication, and false. Similarly you can prove that proof by contraction, i.e. double negation elimination ¬ ¬A -> A is a theorem of constructive logic whenever A is a formula that does not use the constructive disjunction or constructive existential (where negation is defined in terms of implication and false).
For the all of the above, I'm particularly focused on first-order number theory, however all of the above carries over to higher-order theories, and I think it even holds for set theory (or at least some large part of set theory such as Zermelo set theory; I forget what happens with the replacement axiom). Higher-order constructive mathematics does come with the caveat that the Axiom of Choice is not a theorem of constructive mathematics even when it is phrased only using the classical existential.
[1]https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%...
[0]: https://en.wikipedia.org/wiki/Diaconescu%27s_theorem#:~:text....