I think people like author are positive about us, humanity, being able to build AI or something being very close to that.<p>I am not.<p>From the energy efficiency perspective human brain is very, very effective computational machine. Computers are not. Thinking about scale of infrastructure of network of computers being able to achieve similar capabilities and its energy consumption... it would be enormous. With big infrastructure comes high need of maintenance. This is costly and requires a lot of people just to prevent it from breaking down.
With a lot of people being in one place, there socioeconomical cost, production, transportation needs to be build around such center.
If you have centralized system, you are prone to attack from adversaries.
In short I do not think we even close to what author is afraid of. We just closer to beginning to understand what is the need to actually start to think about building AI - if ever possible at all.
I love the language of this article :-)... it may be florid, but that's quintessentially human.<p>About the substance, I agree that there are fair grounds for concern, and it's not just about mathematics.<p>The best case scenario is rejection and prohibition of uses of AI that fundamentally threaten human autonomy. It is theoretically possible to do so, but since capital and power are pro-AI[^1], getting there requires a social revolution that upends the current world order. Even if one were to happen, the results wouldn't last for too long. Unless said revolution were so utterly radical that would set us in a return trajectory to the middle ages (I have something of the sort published somewhere, check my profile!).<p>I'm an optimist when it comes to the enabling power of AI for a select few. But I'm a pessimist otherwise: if the richest nation on Earth can't educate its citizens, what hope is there that humans will be able to supervise and control AI for long? Given our current trajectory, if nothing changes, we are set for civilization catastrophe.<p>[^1]: Replacing expensive human labor is the most powerful modern economic incentive I know of. Money wants, money gets.
The camera didn't kill painting. Neither the bicycle nor the motor-car killed running. There are already subfields of mathematics where it's believed that all the interesting discoveries have been found and no-one is looking except for the occasional amateur - and other subfields where to even have a hope of doing cutting edge research you would need to both do multiple years of postgraduate study and then get accepted onto one of a small number of close-knit teams that are pushing that cutting edge on an industrial scale.<p>So I don't see any reason to worry about the impact of AI. Unlike most fields with AI worries, mathematical research isn't even a significant employment area, and people with jobs doing it could almost certainly be doing something else for more money.
The terrifying thing about lean and machine learning is not the idea that we will train computers on human written proof, but that we won't have to. With the rules of chess easily computed, a computer can use the bellman equations and self play to learn a policy that is vastly superior to human play, at least on the critical path.<p>The state space of mathematics is pretty different from chess, but I think ultimately, mathematicians are just running something like A* on the space of propositions, with a custom heuristic <i>that is learned by approximating the result of running A* with that heuristic</i>. where your error is just the difference between the actual and predicted length of proof.
Considering that mathematics is, at its core, a language for defining relationships between quantities, and then relationships between those relationships, so on and so forth, I think it's fair to assume that the possible number of such relationships are infinite. Some of these relationships will obviously be useful in the real world, but they don't always have to be. I too, suspect that we can keep on building theorems on top of theorems with increasing complexity, until a point is reached that it becomes just too tedious (but not impossible) for a human being to work through the proof.
"perhaps advanced ML research models will be more analogous to improvements in climbing gear, aiding the development of mountaineering as a sport, than an intrusion of corporate control into our minds". I would argue that GPS and Satellite-connected phones are already poisoning the wilderness experience.
Test-driven development is not about tests. It's about writing code. The tests are there just in order to keep the bugs away.<p>Mathematics is just proof-driven development. For an spectator it might look like mathematics is about writing proofs, but that's not different than seeing a software developer write a lot of tests. The proofs are the best tools against insidious logic bugs that the society of mathematics has come up with in the last few hundred years. Mathematicians would welcome automating all the proofs, just like software engineers are happy for code assistants to take over the task of writing tests.
We'll know that the time draws nearer when an AI confirms or refutes Mochizuki's proof of the <i>abc</i> conjecture. As of right now, I don't think they're capable of doing that. And, as they can't even check a very (very!) complex proof, they won't be able to conjure any inhumanly complex proofs <i>de novo</i>.<p>Also:<p>> <i>To expand: what if the practice of mathematics becomes completely determined by the diktats of a vast capitalist machinery of proprietary machine learning models churning out proof after proof, and theory after theory, conjured from the aether of all possible true statements?</i><p>I don't think that this is possible even in theory, as computational resources are limited and "the aether of all possible true statements" is incomprehensively vast. (There's a massive orders-of-magnitude difference in size between true-seeming-yet-false statements and the number of elementary particles in the visible universe. More statements than particles.) You can't brute force it.
I don’t share the author’s concern about a corporate takeover of mathematics. Most mathematics isn’t of commercial interest. Even when it is, it seems like there would often good reason to share it, like any other source code. Is Lean so different from other programming languages?<p>Such libraries would need documentation, or nobody would know when to use them, and then sharing is pointless.<p>If corporations build them, they would have to decide what to contribute to the commons and what to keep private. But that’s no different than any other language.
This article is written in an unnecessarily extravagant style, IMO.<p>Also, I appreciate anonymity, but, to my point<p>> I live by myself in a remote mountain cave beyond the ken of civilised persons, and can only be contacted during a full moon, using certain arcane rites that are too horrible to speak of.<p>Okay.