Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

The fall of the theorem economy

davidbessis.substack.com

Post reply on HN
Print view View original

31–40 of 127 posts

Re: The fall of the theorem economy

#31

Post by olooney »

Greg Egan's description of how mathematics evolves into "truth mining" in his novel Diaspora is seeming more and more prescient. It essentially describes what mathematics would look like after formalization records all theorems discovered so far in a huge, collective database and proof assistants can instantly work out the details of a given proof. What remains of mathematics? According to Egan, visualization, intuition, and insight.

One of the most fruitful approaches in mathematics is to flip back and forth between geometric and algebraic views of a problem. I think this works so well because these are actually handled by two different parts of the brain on a physical level; spatial reasoning is separate from language processing. Cytoarchitecture shows these regions have different "textures;" the local details of the way neurons are wired together are simply different in these different regions of the brain, in the same way a CNN and a transformer have different topologies. Thus, by flipping problems from geometry to algebra and vice versa, we're able to bring an entirely different cognitive style to bear on a problem. For example, the proof of Monge's Theorem by moving to 3D and visualizing not three circles, but three spheres sitting on a table with a book on top of them and then pointing out that the intersection of two planes is a line. What is pages of unintuitive symbol pushing turns into something a child can understand. Going the other way, things like the angle addition formulas or the quadratic formula, which are quite hard to prove geometrically, become quite simple if you use a little algebra.

Current-gen LLMs are still relatively weak at visual reasoning; see the Vision Language Models are Blind paper, for example, or the ARC-AGI benchmark. So that's one way humans can stay ahead of the agents, at least for now.

Re: The fall of the theorem economy

#32

Post by twoodfin »

bsenftner wrote: post #9

This kills me, it is correct, but misses the forest for the trees. Yes, mathematics is a discipline of understanding, but an insular one. The entire field is about trying to understand, but the discipline does not try to be understood. No, that is "your job, not theirs" and that is why this discipline is struggling, struggling in a culture that can barely communicate without emotional morons destroying any constructi…

Eh? I thought this was the main thrust of the argument: Mathematics has in fact always prized conceptual advancement and understanding over proof, despite presenting itself internally and externally as rewarding the latter. The author calls what he’s proposing “rebranding a plurimillenial project”.

Re: The fall of the theorem economy

#33

Post by throwaway91827 »

Staross wrote: post #17

I thought it was very interesting, but maybe also incredibly naive politically ? it's like he's re-discovering alienation under capitalism. A wood-worker could do the same argument, there's the "official" wood-working word of perfect joinery and beautifully finished tables one can buy, but behind it there's the "secret" messy human element, the art, the craft, the mistakes and hard-ships, the elevation of human skill…

I don't think you have it right- the analogy to woodworking and craftsmanship is a category error and probably misses the broad thrust of the essay.

The goal of a woodworker or craftsman is the production of a finished good. He's arguing that, although it's been convenient to position a mathematician as a "theorem-producer", that's never really been the aim of mathematics, and that the actual products of mathematics are some kind of "mental software"- see his references to neuroplasticity. Basically, he's saying that the goal of mathematics is to create abstract structures that allow humans to reason about increasingly complex concepts, and that the "mathematician as theorem producer" is more like a convenient fiction that mathematicians have allowed to persist for too long, and now threatens to endanger the whole practice of mathematics.

Re: The fall of the theorem economy

#34

Post by tux3 »

rbanffy wrote: post #24

> to come up with a conceptual framework where it became easy to express Feels a lot like building software from bottom - once you get the building blocks defined right, the action, or the program, are trivial to express. When doing it from the top-down, you write the program using the building blocks you haven't defined yet, and you might end up with overly specific building blocks, needing other blocks for expressi…

Well, it depends. Sometimes in math you do a lot of chipping away at a problem, and eventually a bigger result falls after all the right foundations are built. That seems to describe bottom-up building.

On the other hand when a new high-level concept becomes clear and seems to emerge like a revelation, and people start thinking in terms of those new definitions, it seems that a hundred pages worth of smaller results can fall out of it almost effortlessly. This way of describing it is more top-down.

I don't know that there's an exact parallel with software. Math keeps feeding into itself in a way that software dreams about with our ambitions of code reuse. The old Object Oriented dreams of perfectly encapsulated classes and abstractions partially worked out, but not to the degree that was envisioned.

The current situation with package managers doesn't look like a tower that keeps growing higher and higher levels of abstractions. It looks like a tower where each person wants to place one tiny brick that they call left-pad, and next year we will rebuild the lower levels instead of going higher. So the top-down and bottom-up building that we do is different. We keep rebuilding the bottom, and we don't very much like when the tower of abstractions get too tall and hard to maintain.

Re: The fall of the theorem economy

#35

Post by tux3 »

rbanffy wrote: post #24

> to come up with a conceptual framework where it became easy to express Feels a lot like building software from bottom - once you get the building blocks defined right, the action, or the program, are trivial to express. When doing it from the top-down, you write the program using the building blocks you haven't defined yet, and you might end up with overly specific building blocks, needing other blocks for expressi…

Well, it depends. Sometimes in math you do a lot of chipping away at a problem, and eventually a bigger result falls after all the right foundations are built. That seems to describe bottom-up building.

On the other hand when a new high-level concept becomes clear and seems to emerge like a revelation, and people start thinking in terms of those new definitions, it seems that a hundred pages worth of smaller results can fall out of it almost effortlessly. This way of describing it is more top-down.

I don't know that there's an exact parallel with software. Math keeps feeding into itself in a way that software dreams about with our ambitions of code reuse. The old Object Oriented dreams of perfectly encapsulated classes and abstractions partially worked out, but not to the degree that was envisioned.

The current situation with package managers doesn't look like a tower that keeps growing higher and higher levels of abstractions. It looks like a tower where each person wants to place one tiny brick that they call left-pad, and next year we will rebuild the lower levels instead of going higher. So the top-down and bottom-up building that we do is different. We keep rebuilding the bottom, and we don't very much like when the tower of abstractions get too tall and hard to reason about.

Re: The fall of the theorem economy

#36

Post by rjsw »

aleph_minus_one wrote: post #23
stackbutterflow wrote: post #15

Tangential but this article got me thinking. Are we going to see less publicly shared science? With private actors or governments restricting access to AI resources to a few scientists and keeping new knowledge to themselves. Advancing science in the open was the best strategy when there was real advantage to share the load with every brain on the planet willing to give a try at science, but if a computer can match o…

> to share the load with every brain on the planet willing to give a try at science This is what a lot of scientists love to tell themself or talk about in celebratory speeches. The truth is: a lot of science is kept behind journal paywalls, so that only "officially approved" (in the sense of: working at a university or an governmental research institute) scientists can easily access it.

People are working on using LLMs to regenerate experimental data from the text of journal papers.

Re: The fall of the theorem economy

#37

Post by a1o »

From reading this, it looks like the projected future is mathematicians working more applied to a domain, and the basic research in the academia being severely impacted by the AI companies - who have the money to hire the senior mathematicians from the academia. I guess if some of the biggest universities could come up with their own AI powered programs there could be something to “answer” in a more accessible knowledge, but I don’t see how to properly keep the students motivated to ensure the field keeps producing new people.

Re: The fall of the theorem economy

#38

Post by lelanthran »

accurrent wrote: post #22
stackbutterflow wrote: post #15

Tangential but this article got me thinking. Are we going to see less publicly shared science? With private actors or governments restricting access to AI resources to a few scientists and keeping new knowledge to themselves. Advancing science in the open was the best strategy when there was real advantage to share the load with every brain on the planet willing to give a try at science, but if a computer can match o…

The intelligence is only one part of the story. People need to actually go out there and do experiments. Science is not only theory, but also experimental. The best science happens when experiments show that a previously held assumption was not true. Eg the Michaelson Morley experiment where the assumption of ether was disproved. While AI is an incredibly powerful tool, it does not replace the act of observation. Thu…

> People need to actually go out there and do experiments. Science is not only theory, but also experimental.

For biosciences and physics, sure. For mathematics? I am skeptical that your assertion applies.

Re: The fall of the theorem economy

#39

Post by rramadass »

guelo wrote: post #20

When math is so divorced from science and engineering that there's no conceivable way that it will ever be applied in the real world then it is just a complex puzzle game that a tiny group of people play. It doesn't really matter much. If the 200,000 line Mathslop proof has no real world application and it doesn't help the puzzle solvers then it is double useless.

Right; this is my viewpoint too. All the "pure mathematicians" have a bleak future where AI can do all the puzzle solving better and faster. They existed in their own world elevating "theorem proving within a formal system" as the central aspect of "proper" mathematics and everything else as ancillary.

It always felt wrong to me that while the scientific method iterated starting with the "real world" viz. Observe, Measure, Hypothesize (includes modeling with mathematics), Test and Refine; pure mathematicians lost themselves in the formalization of hypothesizing/modeling and thus lost touch with mapping it to reality. The AI revolution is now showing them up.

Re: The fall of the theorem economy

#40

Post by accurrent »

lelanthran wrote: post #38
accurrent wrote: post #22

Earlier quoted context omitted.

The intelligence is only one part of the story. People need to actually go out there and do experiments. Science is not only theory, but also experimental. The best science happens when experiments show that a previously held assumption was not true. Eg the Michaelson Morley experiment where the assumption of ether was disproved. While AI is an incredibly powerful tool, it does not replace the act of observation. Thu…

> People need to actually go out there and do experiments. Science is not only theory, but also experimental. For biosciences and physics, sure. For mathematics? I am skeptical that your assertion applies.

Ah I see your point, I took the word science to mean bio, physics, chemistry, etc. IMO mathematics is a different discipline and not one Id consider a science, rather I see it as the language with which we express science.

If AI is somehow able to prove everything wouldn't it bypass Godel's incompleteness theorems?

Post reply on HN