AI in mathematics is forcing big questions • Hacker News Board

Re: AI in mathematics is forcing big questions

#191

Post by godelski » Tue, Jun 30, 2026, 2:19 AM UTC

zmgsabst wrote: post #59

godelski wrote: post #55

Earlier quoted context omitted.

> In some sense I always considered programming to be more trustworthy than maths arguments without the certainty of a solver proof. But programming is a subset of mathematics. They are both formal languages. I suspect the trustworthiness is more in your comfort level than the ability to verify

That depends on who you ask. Type theory can also be an independent synthetic foundation atop which you build mathematics.

You can build all of mathematics on type theory? I very much doubt that considering there isn't even a fully unified mathematics. There's holes that don't know how to be bridged between entire subfields. So I'd be impressed if type theory really could do everything, but hey, I don't know

Re: AI in mathematics is forcing big questions

#192

Post by _zoltan_ » Tue, Jun 30, 2026, 9:25 AM UTC

crote wrote: post #139

_zoltan_ wrote: post #91

Earlier quoted context omitted.

there is a difference but it's overrated. if a theorem is proven, then, as OP said, the theorem is the interface, no matter where the proof is. just as we don't re-prove Fermat's little theorem every time I use it in a proof, because well, it's a theorem.

> just as we don't re-prove Fermat's little theorem every time I use it in a proof Exactly! There's a shared foundation, and everyone builds upon it. A mathematical paper is a whole bunch of Lego blocks being added to that foundation, and combining them in a hopefully-useful new interface. But if the entire paper is just one giant black box, you only get to use the final interface: you lose the ability to meaningfull…

I just wanted to commend you on this analogy. Very nice. Thank you!

Re: AI in mathematics is forcing big questions

#193

Post by morpheos137 » Thu, Jul 02, 2026, 2:19 PM UTC

esafak wrote: post #50

morpheos137 wrote: post #38

Much can be resolved when it is understood math is discovered not created. AI is a tool. if it makes discovery or proof easier that is still mathematics. A proof stands on its own logic regardless how it is derived. The root concern is how ai may provide uplift for mathematical discovery outside of socially expected channels.

You're not concerned about mathematics disappearing as a profession?

It won't. Did automation cause people to stop working in the textile industry?