2 ms·

It's not a secret. It's what makes it so impenetrably annoying that the smartest people move on to problems they can have more of an impact on, casting suspicio

It's not a secret. It's what makes it so impenetrably annoying that the smartest people move on to problems they can have more of an impact on, casting suspicion on anyone who survives in the current establishment. There was a post the other day from stopa.io about implemeting Russel and Whitehead's "Principia" in LISP, and then describing Godel's theorems relative to it, that to me was the future of maths. I'd posit that math is in the midst of the equivalent of the AI winter of the 80's and 90's, where current establishment thinking will be subsumed by practitioners just making shit work as the result of a generation of kids with access to things like Coq, theorem provers, and a bunch of hackers using functional languages, just like "AI" happened as the result of some adequate tooling available to people without gatekeepers. I think we're on the precipice of a rennaisance.

ravi-delia 4y ago
There's been a ton of great work in math lately! I mean in number theory alone we have tools which would have made the greats of the past weep with joy, and we've only just begun to scratch the surface of what they can do. Implementing a formalism that frankly does not have a significant impact on any area of math which isn't directly based on working with it is not a sign that math as a whole is trending towards programming. Theorem solvers are, obviously, getting more awesome by the day though. Not quite there yet, but damn are they close
- motohagiography 4y ago
  Indeed, it's not that math is trending toward programming, but programmers are trending toward math, which means more minds on the problems acquiring the tools. It's exciting to read about too. Quanta has some of the best writing I've ever read anywhere. I am a layman who is enthusiastic about it and sees the most important problem to solve as being how to scale to new minds faster. The most influential people in my own life were not the best at what they did, but the ones who let on that the bar to doing those things and being a part of the conversation was closer and more achievable than the headlines about virtuosos made it appear. We're only ever 3-5 years from learning anything, imo, and I think a lot of the opportunity to have an impact will be in writing the next GEB, Chaos, Emperor's New Mind, or other popular treatment, where instead of focusing on and solving one problem, we can inspire and apply a million new minds to several of them.
ahelwer 4y ago
There's an enormous amount of work to do before what you're saying can be possible. All of existing mathematics has to be encoded as a wikipedia-style library in whatever flavor of theorem prover will win this round (Coq? Lean?) and as someone who has taken a decent run at encoding some theorems - it is non-trivial, both in terms of learning the theorem prover language, learning the math, and learning how to translate the math into the theorem prover language. The number of people worldwide who currently have the skills to do this probably number in the hundreds, and all of them are faced with the choice of contributing theorems or working incredibly lucrative finance/software jobs - or just researching novel mathematics! Even once the library is complete a huge amount of work remains to get using theorem provers to the same level of ergonomics as sketching things out on a chalk board.

ravi-delia 4y ago

There's been a ton of great work in math lately! I mean in number theory alone we have tools which would have made the greats of the past weep with joy, and we've only just begun to scratch the surface of what they can do. Implementing a formalism that frankly does not have a significant impact on any area of math which isn't directly based on working with it is not a sign that math as a whole is trending towards programming. Theorem solvers are, obviously, getting more awesome by the day though. Not quite there yet, but damn are they close

motohagiography 4y ago
Indeed, it's not that math is trending toward programming, but programmers are trending toward math, which means more minds on the problems acquiring the tools. It's exciting to read about too. Quanta has some of the best writing I've ever read anywhere. I am a layman who is enthusiastic about it and sees the most important problem to solve as being how to scale to new minds faster. The most influential people in my own life were not the best at what they did, but the ones who let on that the bar to doing those things and being a part of the conversation was closer and more achievable than the headlines about virtuosos made it appear. We're only ever 3-5 years from learning anything, imo, and I think a lot of the opportunity to have an impact will be in writing the next GEB, Chaos, Emperor's New Mind, or other popular treatment, where instead of focusing on and solving one problem, we can inspire and apply a million new minds to several of them.

ahelwer 4y ago

There's an enormous amount of work to do before what you're saying can be possible. All of existing mathematics has to be encoded as a wikipedia-style library in whatever flavor of theorem prover will win this round (Coq? Lean?) and as someone who has taken a decent run at encoding some theorems - it is non-trivial, both in terms of learning the theorem prover language, learning the math, and learning how to translate the math into the theorem prover language. The number of people worldwide who currently have the skills to do this probably number in the hundreds, and all of them are faced with the choice of contributing theorems or working incredibly lucrative finance/software jobs - or just researching novel mathematics! Even once the library is complete a huge amount of work remains to get using theorem provers to the same level of ergonomics as sketching things out on a chalk board.