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

AlphaProof's Greatest Hits

rishimehta.xyz

Post reply on HN
Print view View original

111–120 of 140 posts

Re: AlphaProof's Greatest Hits

#111

Post by tucnak »

sega_sai wrote: post #40

I think the interface of LLM with formalized languages is really the future. Because here you can formally verify every statement and deal with hallucinations.

Grammar sampling has been around for months, and remained largely unexplored. Don't fall into the common trap of thinking in a fixed language, rather think about a superset of possible languages (grammars) and how they could evolve from one another. I bet, if there's a breakthrough, it's probably in "differential grammars," or whatever it would be called: plug that into the backtracking sampler, & you have your System 2.

Re: AlphaProof's Greatest Hits

#112

Post by empath75 »

throwaway713 wrote: post #39

Anyone else feel like mathematics is sort of the endgame? I.e., once ML can do it better than humans, that’s basically it?

Computers have been better than us at calculation since about a week after computers were invented.

If a computer proves the Reimann Hypothesis, someone will say "Oh of course, writing a proof doesn't require intelligence, it's merely the dumb application of logical rules, but only a human could have thought of the conjecture to begin with."

Re: AlphaProof's Greatest Hits

#113

Post by looofooo0 »

jdietrich wrote: post #77
throwaway713 wrote: post #39

Anyone else feel like mathematics is sort of the endgame? I.e., once ML can do it better than humans, that’s basically it?

Humans are terrible at anything you learn at university and incredibly good at most things you learn at trade school. In absolute terms, mathematics is much easier than laying bricks or cutting hair. https://en.wikipedia.org/wiki/Moravec%27s_paradox

Sure but checking everything is correctly wired, plug-in, cut etc. Everything needes is thought of? There is plenty of things an AI could do to help a trades man.

Re: AlphaProof's Greatest Hits

#114

Post by empath75 »

nybsjytm wrote: post #27
dash2 wrote: post #22

Earlier quoted context omitted.

Though, if you start solving problems that humans can't or haven't solved, then questions of capacity won't matter much. A speedup in the movement of the maths frontier would be worth many power stations.

For some time a 'superhuman math AI' could be useful for company advertising and getting the attention of VCs. But eventually it would be pretty clear that innovative math research, with vanishingly few exceptions, isn't very useful for making revenue. (I am a mathematician and this is meant with nothing but respect for math research.)

The big exception being predicting market movements, and I can't imagine how much money the hedge funds are spending on this right now.

Re: AlphaProof's Greatest Hits

#115

Post by empath75 »

uptownfunk wrote: post #10
wslh wrote: post #3

If you were to bet on solving problems like "P versus NP" using these technologies combined with human augmentation (or vice versa), what would be the provable time horizon for achieving such a solution? I think we should assume that the solution is also expressible in the current language of math/logic.

The hard part is in the creation of new math to solve these problems not in the use of existing mathematics. So new objects (groups rings fields) etc have to be theorized, their properties understood, and then that new machinery used to crack the existing problems. I think we will get to a place (around 5 years) where AI will be able to solve these problems and create these new objects. I don’t think it’s one of tech…

> I think we will get to a place (around 5 years) where AI will be able to solve these problems and create these new objects.

For all we know, buried deep in AlphaProof's attempts to solve these toy problems, it already tried and discarded several new ideas.

Re: AlphaProof's Greatest Hits

#117

Post by Tainnor »

Xcelerate wrote: post #44
E_Bfx wrote: post #36

Earlier quoted context omitted.

I guess it is tautological from the definition of "provable". A theorem is provable by definition if there is a finite well-formulated formula that has the theorem as consequence ( https://en.wikipedia.org/wiki/Theorem paragraph theorem in logic)

Not sure it’s a tautology. It’s not obvious that a recursively enumerable procedure exists for arbitrary formal systems that will eventually reach all theorems derivable via the axioms and transformation rules. For example, if you perform depth-first traversal, you will not reach all theorems. Hilbert’s program was a (failed) attempt to determine, loosely speaking, whether there was a process or procedure that could…

It's "obvious" in the sense that it's a trivial corollary of the completeness theorem (so it wouldn't be true for second order logic, for example).

Hilbert's program failed in no contradiction to what GP wrote because the language of FOL theorems is only recursively enumerable and not decidable. It's obvious that something is true if you've found a proof, but if you haven't found a proof yet, is the theorem wrong or do you simply have to wait a little longer?

Re: AlphaProof's Greatest Hits

#118

Post by staunton »

kzrdude wrote: post #108
chvid wrote: post #102

Mathematicians have been using computers, programming languages, and proof engines for over half a century; however breakthroughs in mathematics are still made by humans in any meaningful sense, even though the tools they use and make are increasingly complex. But as things look now, I will be willing to bet that the next major breakthrough in maths will be touted as being AI/LLMs and coming out of one of the big US…

But, these AI solutions are trying to solve math problems to prove their AI capabilities, not because they care about mathematics.

Sure. Why do you say "but"? Solving such a math problem (while perhaps massively overstating the role AI actually played in the solution) would be great PR for everyone involved.

Re: AlphaProof's Greatest Hits

#119

Post by staunton »

youoy wrote: post #98
jdietrich wrote: post #77

Earlier quoted context omitted.

Humans are terrible at anything you learn at university and incredibly good at most things you learn at trade school. In absolute terms, mathematics is much easier than laying bricks or cutting hair. https://en.wikipedia.org/wiki/Moravec%27s_paradox

I would say that "narrow" mathematics (finding a proof of a given statement that we suspect has a proof using a formal language) is much easier that "generally" laying brick or cutting hair. But I cannot see how consistently doing general mathematics (as in finding interesting and useful statements to proof, and then finding the proofs) is easier than consistently cutting hair/driving a car. We might get LLM level ma…

> But I cannot see how consistently doing general mathematics (as in finding interesting and useful statements to proof, and then finding the proofs) is easier than consistently cutting hair/driving a car.

The main "absolute" difficulty there is in understanding and shaping what the mathematical audience thinks is "interesting". So it's really a marketing problem. Given how these tools are being used for marketing, I would have high hopes, at least for this particular aspect...

Re: AlphaProof's Greatest Hits

#120

Post by [deleted] »

nybsjytm wrote: post #68
sega_sai wrote: post #40

I think the interface of LLM with formalized languages is really the future. Because here you can formally verify every statement and deal with hallucinations.

If this were the case, I don't see why we'd need to wait for an AI company to make a breakthrough in math research. The key issue instead is how to encode 'real-life' statements in a formal language - which to me seems like a ludicrous problem, just complete magical thinking. For example, how might an arbitrary statement like "Scholars believe that professional competence of a teacher is a prerequisite for improving…

[deleted]
Post reply on HN