4 ms·

I am not a mathematician. But long term I think the #1 most important project is something like mathlib: https://leanprover-community.github.io/ https://leanpr

by jnash 4y ago

I am not a mathematician. But long term I think the #1 most important project is something like mathlib: https://leanprover-community.github.io/ https://leanprover-community.github.io/ I think it is the future of mathematics. Yes I know that 99% of mathematicians will disagree. That's not unusual for a fundamental change to how people think. And yes I know it will take a very long time for this change to manifest itself. That is also not unusual for a fundamental change to how people think. But don't underestimate the exponential power of real formal mathematics. What mathematicians are currently calling "formal" proofs aren't. They are just informal proofs with lots of details. Again, 99% of mathematicians will strongly disagree. However eventually we will see math journals dedicated to formally proven correct mathematics. And those proof will start to be regarded above and beyond the current informal proofs. It will take a long time. But IMHO it is inevitable.

destring 4y ago
Can’t help but laugh at the phrase “Real formal mathematics”. Mathematics are as formal as required to be understood by the audience. After all, math is just a way to communicate abstract arguments and reasoning. Computers require more help to understand abstract concepts, doesn’t mean that formulation is better than our current one. See Principia Mathematica on why too much formalism is not a good idea.
- jnash 4y ago
  Can't help but laugh at your comment. Mathematics is an informal social activity where humans try to convince other humans that certain abstract structures have certain properties. Having to turn those proofs into formal machine checked proofs makes a huge difference. Principia Mathematica was a big step forward and directly leading to Type Theory. It didn't succeed in what the authors tried to accomplish, but it very much had a massive impact on the world of mathematics. That's why we both know about it and discuss it today.

by jnash 4y ago

destring 4y ago

Can’t help but laugh at the phrase “Real formal mathematics”. Mathematics are as formal as required to be understood by the audience. After all, math is just a way to communicate abstract arguments and reasoning. Computers require more help to understand abstract concepts, doesn’t mean that formulation is better than our current one. See Principia Mathematica on why too much formalism is not a good idea.

jnash 4y ago
Can't help but laugh at your comment. Mathematics is an informal social activity where humans try to convince other humans that certain abstract structures have certain properties. Having to turn those proofs into formal machine checked proofs makes a huge difference. Principia Mathematica was a big step forward and directly leading to Type Theory. It didn't succeed in what the authors tried to accomplish, but it very much had a massive impact on the world of mathematics. That's why we both know about it and discuss it today.