41–50 of 275 posts
> When he told colleagues the nature of Scholze and Stix’s objections, he wrote, his descriptions “were met with a remarkably unanimous response of utter astonishment and even disbelief (at times accompanied by bouts of laughter!) that such manifestly erroneous misunderstandings could have occurred.” Is this normal in advanced Math or is this guy kind of a jerk?
I have a MSc in mathematics so I am by no means an expert in mathematics proofs but I get the gist of it. To me a proof is literally a logical argument that you can follow to "believe" that a theorem is true. I do worry how many people actually understand or verify mathematics proofs. How many people have actually read and verified Perelman's or Wiles' proofs (I'm only singling them out because they're famous, not be…
The really interesting case here is Voevodsky, who found an error in one of his own proofs many years later and then got interested in foundations of Mathematics and automated proofs. Homotopy type theory is an interesting development, particularly if you are into programming languages.
https://galoisrepresentations.wordpress.com/2017/12/17/the-a... Terence Tao and Peter Scholze (and others) join the discussion in the comments section.
Tao's commentary is especially interesting for me as a non-mathematician: >It seems bizarre to me that there would be an entire self-contained theory whose only external application is to prove the abc conjecture after 300+ pages of set up, with no smaller fragment of this setup having any non-trivial external consequence whatsoever. Likely such is the understatement-ish way of a mathematician to say "This is clearly…
Important conjecture like ABC expressess some fundamental feature in the field. It's not just a arbitrary brainteaser. How to solve this one problem should give insights to many related problems.
Thought experiment:
Imagine a modern mathematician/time traveller who want's to impress Carl Friedrich Gauss by solving problems CFG can't solve, but at the same time the not wanting to give away any clues to modern mathematics. Traveler would need to devise complex and convoluted ways to proof things. Proofs would probably piss off GFG more than impress him.
Earlier quoted context omitted.
The really interesting case here is Voevodsky, who found an error in one of his own proofs many years later and then got interested in foundations of Mathematics and automated proofs. Homotopy type theory is an interesting development, particularly if you are into programming languages.
I don't really understand why the entire known mathematics is not automatically proven yet. We, people, understand very formal proofs. Mathematics is very strict science with axioms and following theorems. It should be a perfect application for computing. I'm not talking about computer prooving theorem himself, but mathematician should write proof using some formal language and computer should be able to follow that…
(This might be one reason, from https://en.wikipedia.org/wiki/Mathematical_proof#Computer-as... )
Earlier quoted context omitted.
The really interesting case here is Voevodsky, who found an error in one of his own proofs many years later and then got interested in foundations of Mathematics and automated proofs. Homotopy type theory is an interesting development, particularly if you are into programming languages.
I don't really understand why the entire known mathematics is not automatically proven yet. We, people, understand very formal proofs. Mathematics is very strict science with axioms and following theorems. It should be a perfect application for computing. I'm not talking about computer prooving theorem himself, but mathematician should write proof using some formal language and computer should be able to follow that…
I have a MSc in mathematics so I am by no means an expert in mathematics proofs but I get the gist of it. To me a proof is literally a logical argument that you can follow to "believe" that a theorem is true. I do worry how many people actually understand or verify mathematics proofs. How many people have actually read and verified Perelman's or Wiles' proofs (I'm only singling them out because they're famous, not be…
From page 6 with figure 1, to page 10 with figure 3, it's clear that even just changing to structured proofs over prose proofs can be helpful in catching errors. Of course the rest of the paper goes into detail about going even further... I don't know if Lamport's ideas have gained any more acceptance in the mathematics communities, but I'm doubtful. At least if memory serves the ABC papers were classic prose-style...
Earlier quoted context omitted.
The really interesting case here is Voevodsky, who found an error in one of his own proofs many years later and then got interested in foundations of Mathematics and automated proofs. Homotopy type theory is an interesting development, particularly if you are into programming languages.
I don't really understand why the entire known mathematics is not automatically proven yet. We, people, understand very formal proofs. Mathematics is very strict science with axioms and following theorems. It should be a perfect application for computing. I'm not talking about computer prooving theorem himself, but mathematician should write proof using some formal language and computer should be able to follow that…
Earlier quoted context omitted.
The really interesting case here is Voevodsky, who found an error in one of his own proofs many years later and then got interested in foundations of Mathematics and automated proofs. Homotopy type theory is an interesting development, particularly if you are into programming languages.
I don't really understand why the entire known mathematics is not automatically proven yet. We, people, understand very formal proofs. Mathematics is very strict science with axioms and following theorems. It should be a perfect application for computing. I'm not talking about computer prooving theorem himself, but mathematician should write proof using some formal language and computer should be able to follow that…
> When he told colleagues the nature of Scholze and Stix’s objections, he wrote, his descriptions “were met with a remarkably unanimous response of utter astonishment and even disbelief (at times accompanied by bouts of laughter!) that such manifestly erroneous misunderstandings could have occurred.” Is this normal in advanced Math or is this guy kind of a jerk?
Math academic community is actually very healthy overall, in my experience.
But anyway, mathematics is not any more unhealthy than any other field, but it does have toxicity like all others do as well.
Earlier quoted context omitted.
The really interesting case here is Voevodsky, who found an error in one of his own proofs many years later and then got interested in foundations of Mathematics and automated proofs. Homotopy type theory is an interesting development, particularly if you are into programming languages.
I don't really understand why the entire known mathematics is not automatically proven yet. We, people, understand very formal proofs. Mathematics is very strict science with axioms and following theorems. It should be a perfect application for computing. I'm not talking about computer prooving theorem himself, but mathematician should write proof using some formal language and computer should be able to follow that…
Mathematics textbooks would be intractably longer if they spelled out every step in explicit, formal detail. And then the proofs wouldn't make sense to people because the core ideas would be obscured by the formality! A typical mathematics proof is intended to be read by a thinking human assumed to have some level of mathematical sophistication and knowledge. These assumptions make proofs far more implicit than proofs in a formal language, which essentially only assumes that the "reader", i.e. the computer, can push symbols around and compare them.