41–50 of 125 posts
Earlier quoted context omitted.
AFAIK the advantage of constructivism is algorithms. Coq allows you to extract lisp/ML/Haskell programs. Perhaps we will be seeing the next generation of fully homomorphic encryption programs, or topological data analysis programs, automatically generated by Coq.
So what about an algorithm you verified in a non-constructive way?
Earlier quoted context omitted.
So what about an algorithm you verified in a non-constructive way?
You still need to construct the algorithm in the first place, which is what a constructive proof does.
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.
I think that something like http://us.metamath.org/index.html has already gone a long way in formalizing math. And this is not the only attempt to formalize math, but it is unique that it uses a very limited amount of syntax and rules, and makes use of a simple (small) proof engine, which makes verifying that the proof engine is correct possible.
The problem with metamath is that you basically have to be a fully signed-up masochist in order to do anything nontrivial with it. People have certainly done nontrivial things with it e.g Carneiro and the prime number theorem -- but it takes all sorts. If I want to prove (a+b)(a+2b)(a+3b)= a^3 + 6ba^2 + 11b^2a + 6b^3 in Lean I just type `ring`. Good luck proving that from the axioms of a ring directly in metamath, I…
While it's allowed, generally Metamath users do not prove constructs directly from axioms, for exactly the same reason as you don't do it in Lean or traditional informal mathematics. You're right that most Metamath tools have fewer automated tactics, but there are tools with some automation, and people are working to improve that.
Earlier quoted context omitted.
What is constructive mathematics for the layman?
https://en.wikipedia.org/wiki/Intuitionistic_logic 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 esp…
Earlier quoted context omitted.
Pointing to the top journals is again a statement about who is well-connected, so if anything it is further proof of my claim of elite provincialism. Mathematics has politics, like any other field, and it's politics that determine that the proof of the Robertson-Seymour Theorem appeared in the "Journal of Combinatorial Theory" and not JAMS. The irony is that I suspect every single mathematician, elite or not, knows w…
I think the (implicit) charge that the editors of top journals are keeping good papers out for snobbish reasons is mostly unfounded. I don't deny that their tastes shape what gets published, of course. But in most circumstances, they are not subject matter experts, and the first step of evaluating any paper is that is not an obvious desk-reject (for poor writing, crankery, etc.) is to send it to a group of relevant e…
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
Earlier quoted context omitted.
You still need to construct the algorithm in the first place, which is what a constructive proof does.
Sure, but you would not need to prove it in a constructive way. 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.
Earlier quoted context omitted.
Sure, but you would not need to prove it in a constructive way. 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.
I think we're at cross-purposes; I am talking about mathematics for the purpose of real-life useful applications (e.g. cryptography, data analysis, etc), in which case you need algorithms.
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?
Check out "Automated Propositional Sequent Proofs in Your Browser with Tau Prolog" for a promising approach: https://www.philipzucker.com/javascript-automated-proving/ It's rendering LaTeX proof trees.
I will pay $3.14 to the first person that formalizes mathematics using only https://treenotation.org/ .
But there’s a reason that when writing conditionals, we don’t put each symbol in the expression on their own line. Those also have their own tree structure, they are also part of the AST, but we put many of the nodes on the same line for ease of reading and editing.