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

The cultural divide between mathematics and AI

sugaku.net

Post reply on HN
Print view View original

141–150 of 187 posts

Re: The cultural divide between mathematics and AI

#141

Post by lupire »

mcguire wrote: post #61
nicf wrote: post #8

I'm a former research mathematician who worked for a little while in AI research, and this article matched up very well with my own experience with this particular cultural divide. Since I've spent a lot more time in the math world than the AI world, it's very natural for me to see this divide from the mathematicians' perspective, and I definitely agree that a lot of the people I've talked to on the other side of thi…

Many years ago I heard a mathematician speaking about some open problem and he said, "Sure, it's possible that there is a simple solution to the problem using basic techniques that everyone has just missed so far. And if you find that solution, mathematics will pat you on the head and tell you to run off and play. "Mathematics advances by solving problems using new techniques because those techniques open up new area…

That's the attitude of poor mathematicians who are insecure about their own faults.

Re: The cultural divide between mathematics and AI

#142

Post by mb7733 »

mcguire wrote: post #61
nicf wrote: post #8

I'm a former research mathematician who worked for a little while in AI research, and this article matched up very well with my own experience with this particular cultural divide. Since I've spent a lot more time in the math world than the AI world, it's very natural for me to see this divide from the mathematicians' perspective, and I definitely agree that a lot of the people I've talked to on the other side of thi…

Many years ago I heard a mathematician speaking about some open problem and he said, "Sure, it's possible that there is a simple solution to the problem using basic techniques that everyone has just missed so far. And if you find that solution, mathematics will pat you on the head and tell you to run off and play. "Mathematics advances by solving problems using new techniques because those techniques open up new area…

What the hell is that quote? No, a simple proof is the absolute mathematical ideal!

Re: The cultural divide between mathematics and AI

#143

Post by oersted »

hewtronic wrote: post #138
oersted wrote: post #135

Earlier quoted context omitted.

Yes I definitely concur, I have spent significant time with it. The main bottleneck is having the libraries that define the theorems and objects you need to operate at those levels. Everything is founded on axiomatic foundations and you need to build all of maths on top of that. Projects like mathlib are getting us there but it is a massive undertaking. It’s not just that it is a lot of maths to go through, it’s also…

> Anyways, the complexity of the Lean language itself doesn’t help either. The mode of thinking you need to have to operate it is much closer to programming than maths, and for those that think that the Rust borrow-checker is a pain, this is an order of magnitude more complex. Could you elaborate on this? I'm interested to learn what the complexities are (beyond the mathematical concepts themselves).

Found something I wrote last year, see below, but off the top of my head:

Something like 5 different DSLs in the same language, most of it in a purist functional style that is neither familiar to most mathematicians nor most programmers, with type-checking an order of magnitude more strict and complex than any programming language (that's the point of it), with rather obscure errors most of the time.

It's really tedious to translate any non-trivial proofs to this model, so usually you end up proving it again almost from scratch within Lean, and then it's really hard to understand as it is written. Much of the information to understand a proof is hidden away as runtime data that is usually displayed via a complex VSCode extension. It's quite difficult to understand from the proof code itself, and usually it doesn't look anything like a traditional mathematical proof (even if they kind of try by naming keywords with a similar terminology as in normal proofs and sprinkling some unicode symbols).

I never-ever feel like I'm doing maths when I'm using Lean. I'm fighting with the syntax to figure out how to express mathematical concepts in the style that it likes, always having several different ways of achieving similar things (anti Zen of Python). And I'm fighting with the type-checker to transform this abstract expression into this other abstract expression (that's really what a proof is when it boils down to it), completely forgetting about the mathematical meaning, just moving puzzle pieces around with obscure tools.

And even after all of this, it is so much more ergonomic than the previous generation of proof-assistants :)

---

I think that the main reasons for Lean's complexity are:

- That it has a very purist functional style and syntax, literally reflecting the Curry-Howard Correspondence (function = proof), rather than trying to bridge the gap to more familiar maths notation.

- That it aims to be a proof assistant, it is fundamentally semi-automatic and interactive, this makes it a hard design challenge.

- A lot of the complexity is aimed at giving mathematicians the tools to express real research maths in it, on this it has been more successful than any alternative.

- Because of this it has at least 5 different languages embedded in it: functional expressions of theorems, forward proofs with expression transformations, backward proofs with tactics, the tactics metaprogramming macro language, and the language to define data-types (and at least 4 kinds of data-types with different syntax).

Re: The cultural divide between mathematics and AI

#144

Post by mb7733 »

optimalsolver wrote: post #69
nicf wrote: post #8

I'm a former research mathematician who worked for a little while in AI research, and this article matched up very well with my own experience with this particular cultural divide. Since I've spent a lot more time in the math world than the AI world, it's very natural for me to see this divide from the mathematicians' perspective, and I definitely agree that a lot of the people I've talked to on the other side of thi…

If the shortest proof for some theorem is several thousand pages long and beyond the ability of any biological mind to comprehend, would mathematicians not care about it? Which is to say, if you only concern yourself with theorems which have short, understandable proofs, aren't you cutting yourself off from vast swathes of math space?

> If the shortest proof for some theorem is several thousand pages long and beyond the ability of any biological mind to comprehend, would mathematicians not care about it?

Care or not, what are they supposed to do with it?

Sure, they can now assume the theorem to be true, but nothing stopped them from doing that before.

Re: The cultural divide between mathematics and AI

#146

Post by jlev1 »

cladopa wrote: post #136
the_cat_kittles wrote: post #124

Earlier quoted context omitted.

taking a helicopter to the top of a mountain is not the same thing as climbing it

True. Taking a helicopter is way more impressive. The Everest was climbed in 1953 and the first helicopter to go there was in 2005. It is way harder thing to do.

No, in your analogy building a helicopter capable of going there is impressive. (Though I dispute the idea that it’s more impressive simply because helicopters were invented more recently than mountain climbing.) In any case, riding in a helicopter remains passive and in no sense impressive.

Re: The cultural divide between mathematics and AI

#147

Post by sarchertech »

throw8404948k wrote: post #39
sarchertech wrote: post #26

Earlier quoted context omitted.

I think you’re missing the point of what the advisor is saying.

No, I get it. My point is human advisor does not have enough time, to answer questions and correctly explain the subject. I may get like 4 hours a week, if lucky. Books are just a cheap substitute for real dialog and reasoning with a teacher. Most ancient philosophy papers were in form of dialog. It is much faster to explain things. AI is a game changer. It shortens feedback loop from a week to hour! It makes mistake…

The point is that time and struggle are required for understanding. The advisor isn’t telling the student to go read these books because he doesn’t have time to explain.

He’s saying go read these books, wrestle with the ideas, go to bed, dream about them, think about them in the shower. Repeat that until you understand enough to understand the answer.

There’s no shortcut here. If you had unlimited time with the advisor he couldn’t just sit you down and make you understand in a few sessions.

Re: The cultural divide between mathematics and AI

#148

Post by dartos »

username332211 wrote: post #128
roenxi wrote: post #120

Earlier quoted context omitted.

> I'm fairly sure that people are only getting hung up on the size of this finite set, for no good reason. I think that is exactly correct, except for the "no good reason" part. There aren't many (any?) practical situations where the 4-colour theory's provability matters. So the major reason for studying it is coming up with a pattern that can be used in future work. Having a pattern with a small set (single digit nu…

> So the major reason for studying it is coming up with a pattern that can be used in future work. Surely, reducing the infinite way in which polygons can be placed on a plane to a finite set, no matter how large, must involve some pattern useful for future work?

But why stop at “some” pattern when you can find the most general pattern.

Re: The cultural divide between mathematics and AI

#149

Post by dartos »

myst wrote: post #123
roenxi wrote: post #120

Earlier quoted context omitted.

> I'm fairly sure that people are only getting hung up on the size of this finite set, for no good reason. I think that is exactly correct, except for the "no good reason" part. There aren't many (any?) practical situations where the 4-colour theory's provability matters. So the major reason for studying it is coming up with a pattern that can be used in future work. Having a pattern with a small set (single digit nu…

The nature does not care whether it fits in our brains.

That’s why we use math to describe nature in a way that fits in our brains.

That’s the whole point of math.

Re: The cultural divide between mathematics and AI

#150

Post by whynotminot »

piokoch wrote: post #137
nicf wrote: post #8

I'm a former research mathematician who worked for a little while in AI research, and this article matched up very well with my own experience with this particular cultural divide. Since I've spent a lot more time in the math world than the AI world, it's very natural for me to see this divide from the mathematicians' perspective, and I definitely agree that a lot of the people I've talked to on the other side of thi…

"I can imagine a future where some future model is better at proving theorems than any human mathematician" Please do not overestimate the power of the algorithm that is predicting next "token" (e.g. word) in a sequence of previously passed words (tokens). This algorithm will happily predict whatever it was fed with, just ask Chat GPT to write the review of non-existing camera, car or washing machine, you will receiv…

I can also write you a review of a non-existent camera or washing machine. Or anything else you want a fake review of! Does that mean I’m not capable of reasoning?
Post reply on HN