Mathematics AI Aristotle proves 30 year old Erdos Problem #124 \ stacker news ~AI

pull down to refresh

Mathematics AI Aristotle proves 30 year old Erdos Problem #124

Posted by Robinhood CEO Vlad Tenev regarding his math AI startup Harmonic:

Aristotle from HarmonicMath just proved Erdos Problem #124 in leanprover, all by itself. This problem has been open for nearly 30 years since conjectured in the paper “Complete sequences of sets of integer powers” in the journal Acta Arithmetica.

I'm too dumb to understand what the problem is but it seems legit and even the great Terry Tao has chimed in.

Pretty amazing how quick we've gotten here. I find it rather terrifying personally.

view all related items

84 sats \ 4 replies \ @oliverweiss 30 Nov

Pretty amazing how quick we've gotten here.

Exactly, about two years ago or so, ChatGPT used to make silly mistakes even in (relatively) simple examples. What it can do today is incredible! In a near future, many applied mathematicians (including myself) will be jobless (at least not doing applied math). I’m convinced about that!

66 sats \ 3 replies \ @gmd OP 30 Nov

I'm not really sure what any of us will be doing tbh.

I'm doing some fun vibe-coding right now, which mostly consists of me meta-prompting by asking one AI how to properly state what I want to do, then feeding the much much improved prompt to the other AI. I'm conducting the symphony I suppose by I'm not really sure how much I'm really contributing tbh...

150 sats \ 2 replies \ @optimism 23h

You're providing direction and guidance. We're all CTOs now lol.

Would you see a way to use your vibed code in a live system? What would it take to get it there?

166 sats \ 1 reply \ @gmd OP 23h

Semi live now although haven't publicly shared the URL anywhere (this is the first ever). It's an automated AI driven Technical Analysis tool for degenerate stock market gamblers like me to figure out "what's on sale". Basically helps you buy the dip when you have dry powder (sacrilegious for Bitcoiners, I know! 😂)

https://stockdips.ai/

Last night I was working on implementing concurrent background jobs to perform the LLM calls to execute the Technical Analysis across a large batch of stock tickers. Not only did it code it up for me (not one-shot but close) but it threw up a beautiful dynamic html UI that let me track the job queue in real-time! I thought it would just give me some dirty println text logs to peruse...

Gave me mixed emotions of sadness and wonder.

126 sats \ 0 replies \ @optimism 13h

Looks pretty cool. And SN "launch" is wild! I'm not much into TA or stock markets so I can't really comment on the product itself. I've felt that since TA influences market behavior and TA at the same time references market sentiment then, if a specific analysis gains traction it becomes self-fulfilling - for speculation, not long-term investment of course.

About the process: what this looks like is that you're evolving a tool to automate something you'd do manually (i.e. doing the TA) and then building that out into a suite.

Not only did it code it up for me (not one-shot but close) but it threw up a beautiful dynamic html UI that let me track the job queue in real-time!

The problem with skipping the println stage is of course that you now need to test not only the batch process itself, but also the fancy UI, and you're testing both at once. Thus, because it didn't give you the simple interface, you now have more work at once. This is fine if you didn't plan on doing rigorous testing of course.

42 sats \ 2 replies \ @optimism 30 Nov

At the moment I'm minded to keep this as open, and add the gcd condition in the main statement, and note in the remarks that the easier (?) version allowing 1 and omitting the gcd condition, which was also asked independently by Erdős, has been solved.

21 sats \ 1 reply \ @adlai 30 Nov

source the quote, please...

edit: the reply to this comment has the anchored link, although I was hoping more for something along these lines:

Thomas Bloom, Research Fellow at the University of Manchester.
Creator and maintainer of [erdosproblems.com]

should have made my complaint more specific!

135 sats \ 0 replies \ @0xbitcoiner 30 Nov

https://www.erdosproblems.com/forum/thread/124#post-1895

42 sats \ 9 replies \ @0xbitcoiner 30 Nov

Nerdy stuff! Hahaha

https://www.erdosproblems.com/forum/thread/124

33 sats \ 8 replies \ @gmd OP 30 Nov

I love how one guy (tsaf) in the thread says "Aristotle's solution is as follows. It is surprisingly easy." then proceeds to spit out what to most people is incomprehensible gibberish :P These guys are truly a completely different species of chimp from me.

84 sats \ 6 replies \ @adlai 30 Nov

These guys are truly a completely different species of chimp from me.

you might find this video about one specific AI proof easier for building your intuition, because it focuses on a geometrical problem rather than number theory.

101 sats \ 5 replies \ @gmd OP 30 Nov

I used to have much higher esteem for my mathematics abilities.. sadly medicine robbed my mind of the ability to even calculate tips without significant difficulty 😅

105 sats \ 2 replies \ @adlai 30 Nov

there's a common joke among mathematicians, that as your mathematical mind develops, so does your arithmetic computer atrophy.

I think it's quite understandable; as a mind becomes aware of more useful kinds of numbers¹, and more kinds of patterns² that enable computational tricks, there is a temptation to explore new possibilities rather than charge forth along whichever computational path was learned at a younger age.

I honestly don't think that the capability of reckoning accurately and rapidly in decimal base is worth retaining at grade-school levels. Even if you're e.g. checking over a bill at a restaurant, the important tasks are probably remembering who ordered what and comparing the billed prices to the listed ones, rather than verifying that their point-of-sale performed arithmetic correctly.

most useful kinds are ideals or fields; the most familiar ideals are multiples of any prime, while e.g. "all ratios with a power of two in the denominator" is a field ↩
consider the trick of doubling and shifting the decimal point left, as a shortcut for ~~multiplying~~ dividing by five; it's only the first in an infinite series of similar tricks, for ~~multiplying~~ dividing by powers of five ↩

0 sats \ 1 reply \ @gmd OP 30 Nov

haha Von Neumann must have truly been an alien then!

63 sats \ 0 replies \ @adlai 30 Nov

well some people specifically practice lightning calculation; similarly to how some kid who grew up playing catch might keep on practicing with friends or the next generation, despite not needing the affordance.

I think lightning calculation has always had a bit of an "autistic savant" reputation, because it is so sterile when compared to even things like playing chess or solving a Rubik's Cube.

42 sats \ 1 reply \ @elvismercury 30 Nov

The industry of medicine, or taking medicine? Either way, a cautionary tale.

21 sats \ 0 replies \ @gmd OP 30 Nov

haha memorizing minutiae and constantly reading through vast troves of mostly useless patient information has erased the engineering circuitry in my brain I think (former CS grad)

42 sats \ 0 replies \ @0xbitcoiner 30 Nov

84 sats \ 3 replies \ @adlai 30 Nov

edit: It's doubly unsurprising when you consider how much of what Erdos left mathematics was statements of open problems... his productive time [which was allegedly almost all of his waking hours] was spent either mercilessly roping his friends into coathoring papers with him on his ever-growing list of problems, or brainstorming interesting problems for future papers. So it's much less surprising that an Erdos problem has been attacked successfully, than e.g. a Hilbert problem.

It's not too surprising; lots of the challenges in mathematics are related to comprehensibility, not reachability.

Consider the following thought experiment:

Think of the space of all sequences of all ASCII characters; most of these are noise, right? Not even slop, just noise.

Narrow down the space, radically, to all LaTeX programs; most of these are invalid, or garbage, right? Not even slop, just garbage that you can feed a compiler to heat your computer.

Narrow the space down further, to all LaTeX programs producing renderable documents... still, we're far from anything useful, as this is essentially what the "million monkeys at a million typewriters" produce, although with less animal cruelty.

Now things get interesting: narrow down the space to the LaTeX programs that produce documents beginning with a list of axioms, and continuing with a series of propositions. Most won't be logical, although some tiny vanishing fraction of these will be valid mathematical proofs.

Are any of them proving anything new? Are any of the proofs simpler than the ones found by schoolchildren? Do any of these help us figure out which concepts are worth spending words to name, rather than considering them merely some intermediate noise which lives and dies within the span of one convoluted proof?

33 sats \ 2 replies \ @gmd OP 30 Nov

Interesting perspective... I guess we'll see where we are a year or two from now.

Appears he recently raised $120M for this startup which seems quite a large sum for a mathematics startup... curious how investors expect to get their money back.

21 sats \ 0 replies \ @adlai 30 Nov

Appears he recently raised $120M for this startup which seems quite a large sum for a mathematics startup... curious how investors expect to get their money back.

Off the top of my mind, two possible sources for a finite¹ valuation are the possibility of getting acquired for the technology, and the possibility of selling a service that is used by customers who value mathematical rigor [e.g. aerospace engineers]. I agree that $120M is a lot, especially given how rapidly any bored undergraduate from almost any STEM field could vibe code a theorem proving agent as a semester project by gluing together open source tools.

rather than infinitesimal ↩

21 sats \ 0 replies \ @0xbitcoiner 30 Nov

@remindme in 1 year

42 sats \ 0 replies \ @pbl4eagain 21h

this is awesome and terrifying

42 sats \ 0 replies \ @SimpleStacker 23h

It seems that AI has a harder time getting basic sports facts right than solving math proofs. He just like me fr fr

42 sats \ 0 replies \ @beyond_turbulence 30 Nov

Thanks ! Got subgratance ? #1296293

Footnotes

Footnotes