161–170 of 275 posts
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…
Earlier quoted context omitted.
> Mathematics is very strict science with axioms and following theorems. It should be a perfect application for computing. The short answer is that mathematics is not actually a very good application for computation. It's a rather poor application for computation. Herein lies the rub and the reason why it can't be done as easily as you'd suppose. Computationally-oriented questions and theorems are a subset of all ava…
> That doesn't mean most proofs are wrong, but it does mean that most mathematicians are informal; to the extent they write down proofs of their theorems, they've only ever needed to do so enough to get other mathematicians to say, "Yes, I see what you mean, this does logically follow from what we already both agree on." THIS is the real reason more mathematics isn't computer-checked. You massively buried the lede. >…
I'm not talking about decidability. I'm talking about computability. Real closed fields are decidable, in that a Turing machine can determine in a finite number of steps whether or not a field of real numbers is algebraically closed. But that has no bearing on the fitness of real numbers for computation. Most real numbers are not computable, which is why floating point numbers are only a good enough approximation as I stated.
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…
Agree with this. Don't think there are too many mathematicians who can really argue for or against a really important theorem. My prof has come up with one for Riemann hypothesis[1], but he is not finding anyone willing to engage in a discussion. Most mathematicians seem to believe that the Riemann hypothesis is unsolvable and I don't think it helps that my prof is currently not associated with any reputable universi…
That said, I’d be happy to go over this as an analytic number theorist rfurman@alumni.stanford.edu
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…
\
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…
\
Mathematics is written in a language that is not only precise enough to make it easier to follow logical arguments, but also optimized for human readability. Mysql is written in C, which is optimized in the early days of computing for portability between machines, which is an irrelevant goal to provability. C does not give enough guarantees to prove anything worthwhile, whereas the language of mathematics has been evolving since the 19th century to give as much guarantees as possible. If mysql would be written in agda, it'd be so much more easier to prove it compared to Wiles' proof of Fermat's or whatever. As far as any programming language go, C is probably the worst language you can prove anything let alone mysql.
OP comment wasn't implying proving is supposed to be easy. Mathematics is not written for machines, it's written for humans. Ultimately, the act of writing mathematical papers is not that much different than act of writing sociology papers. A mathematical proof is written so that it convinces a human. Once you start writing those proofs into Coq or agda or whatever, you start seeing how much handwaving is going in mathematics. This is because being experienced in mathematics gives one the ability and confidence to operate on higher levels of abstraction which doesn't need as much precision/rigor as a programming language as context signals the tactic, argument etc...
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.
people with a paper fetish who refuse to believe Maybe there was surprising resistance because you spoke like that?
Nah. I'm only using language that harsh now because of how disappointingly irrational and weak the objections on reddit were. It's odd to see mathematicians resistant to quantifying what they believe to be inferior about computer displays, and improperly generalizing what seemed to be their experience with $500 laptops to also argue against high-quality eInk, OLED and IPS LCDs.
And what Grad student can afford those at [Insert State University]. I was a PhD student in math not long ago, and vastly preferred paper books, and even printed out articles. It is way way easier on your eyes than something actively blasting light. Maybe in 20 years high quality e-ink will be cheap enough, but that has been promised since forever.
Earlier quoted context omitted.
If you've ever tried encoding proofs in a proof assistant such as Coq (which is what the INRIA folks used to encode the four color theorem and the Fiet-Thompson theorem), you'll realise just how painful it is --- I speak as someone who's done this for fun (and now for research. [my report is available here]( https://github.com/bollu/dependence-analysis-coq/blob/master... )
What is the painful part? The level of detail required for it to check?
In other words, it's actually very easy to prove something with a computer, but it's very difficult to prove the thing you actually set out to prove. It's not any easier than writing a bug-free program.
Earlier quoted context omitted.
people with a paper fetish who refuse to believe Maybe there was surprising resistance because you spoke like that?
Nah. I'm only using language that harsh now because of how disappointingly irrational and weak the objections on reddit were. It's odd to see mathematicians resistant to quantifying what they believe to be inferior about computer displays, and improperly generalizing what seemed to be their experience with $500 laptops to also argue against high-quality eInk, OLED and IPS LCDs.
Maybe you don't see the problem because you aren't doing any math?