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

91–100 of 140 posts

Re: AlphaProof's Greatest Hits

#91

Post by auggierose »

nybsjytm wrote: post #49
airstrike wrote: post #41

Earlier quoted context omitted.

"Making revenue" is far from being the only metric by which we deem something worthy.

As a mathematician, of course I agree. But in a sentence like: > A speedup in the movement of the maths frontier would be worth many power stations who is it 'worth' it to? And to what end? I can say with some confidence that many (likely most, albeit certainly not all) mathematicians do not want data centers and power stations to guzzle energy and do their math for them. It's largely a vision imposed from without by…

There is something called applied math, and there is a big gulf between applied math and pure math. This new technology has the potential of making use of much more "pure math" for applied math, unifying much of pure math, applied math, and programming. I don't really care about the RH, I care about that.

Re: AlphaProof's Greatest Hits

#92

Post by benlivengood »

nybsjytm wrote: post #89
benlivengood wrote: post #87

Earlier quoted context omitted.

Probabilistic reasoning is possible in a formal setting; It produces a probability distribution over answers. To ground probabilistic logic itself I'm not aware of much progress beyond the initial idea of logical induction[0]. [0] https://arxiv.org/abs/1609.03543

This takes for granted a formal setting, which is what I'm questioning in any of these 'real world' contexts.

> For example, how might an arbitrary statement like "Scholars believe that professional competence of a teacher is a prerequisite for improving the quality of the educational process in preschools" be put in a lean-like language? What about "The theoretical basis of the October Revolution lay in a development of Marxism, but this development occurred through three successive rounds of theoretical debate"?

> This takes for granted a formal setting, which is what I'm questioning in any of these 'real world' contexts.

A formal model of semantics would likely be a low-level physical representation of possible states augmented with sound definitions of higher-level concepts and objects. I don't think humans are capable of developing a formal semantics that would work for your sentences (it's taken us hundreds of years to approach formalization of particle physics), but I think that an automated prover with access to physical experiments and an LLM could probably start building a more comprehensive semantics.

Re: AlphaProof's Greatest Hits

#93

Post by awanderingmind »

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?

The end of an era perhaps, but not 'the end' - another commenter has already mentioned Moravec's paradox: https://en.wikipedia.org/wiki/Moravec%27s_paradox

It will be interesting if/when these models start proving major open problems, e.g. the Riemann Hypothesis. The sociological impact on the mathematical community would certainly be acute, and likely lead to a seismic shift in the understanding of what research-level mathematics is 'for'. This discussion already appears to be in progress. As an outsider I have no idea what the timeline is for such things (2 years? 10? 100?).

On the plus side, AlphaProof has the benefit over ordinary LLMs in their current form in that it does not pollute our common epistemological well, and its output is eminently interrogable (if you know Lean at last).

Re: AlphaProof's Greatest Hits

#94

Post by auggierose »

nybsjytm wrote: post #20
auggierose wrote: post #17

Earlier quoted context omitted.

Certainly an interesting information that AlphaProof needed three days. But does it matter for evaluating the importance of this result? No.

I agree that the result is important regardless. But the tradeoff of computing time/cost with problem complexity is hugely important to think about. Finding a proof in a formal language is trivially solvable in theory since you just have to search through possible proofs until you find one ending with the desired statement. The whole practical question is how much time it takes. Three days per problem is, by many sta…

> Finding a proof in a formal language is trivially solvable in theory since you just have to search through possible proofs until you find one ending with the desired statement. The whole practical question is how much time it takes.

No, in my experience the whole practical question is, can it be found automatically, or can it not be found automatically? Because there is an exponential search space that conventional automated methods will not be able to chew through, it either works, or it doesn't. AlphaProof shows that for some difficult IMO problems, it works.

Re: AlphaProof's Greatest Hits

#95

Post by j16sdiz »

zeroonetwothree wrote: post #25
Onavo wrote: post #23

Earlier quoted context omitted.

> We know that any theorem that is provable at all (in the chosen foundation of mathematics) can be found by patiently enumerating all possible proofs. Which computer science theorem is this from?

It’s just an obvious statement. If a proof exists, you will eventually get to it.

Only if we take AC, I guess?

Re: AlphaProof's Greatest Hits

#96

Post by ykonstant »

GuB-42 wrote: post #67
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?

Not the endgame by far. Maybe the endgame for LLMs, and I am not even convinced. Maths is detached from reality. An AI capable of doing math better than humans may not be able do drive a car, as driving a car requires a good understanding of the world, it has to recognize object and understand their behavior, for example, understanding that a tree won't move but a person might, but it will move slower than another ca…

>An AI capable of doing math better than humans may not be able do drive a car,

Noo, but my excuse for being unable to drive a car is precisely that I am a quirky mathematician focused on research!

Re: AlphaProof's Greatest Hits

#97

Post by auggierose »

nybsjytm wrote: post #86
nine_k wrote: post #76

Earlier quoted context omitted.

You can't talk about formally verifiable truthiness until you solve epistemology. This can be achieved formally in mathematics, with known principal limitations. Here strict theorem-proving, Lean-style, is viable. It can also be achieved informally and in a fragments way in barely-mathematical disciplines, like biology, linguistics, and even history. We have chains of logical conclusions that do not follow strictly,…

Hmmm I think even in something very nominally nearby like theoretical physics, there's very little that's similar to theorem proving. I don't see how AlphaProof could be a stepping stone to anything like what you're describing. Generally, I think many people who haven't studied mathematics don't realize how huge the gulf is between "being logical/reasonable" and applying mathematical logic as in a complicated proof.…

I don't think that mathematicians are actually in the best position to judge how math/logic might help in practical applications, because they are usually not interested in practical applications at all (at least for the last 70 years or so). Especially, they are also not interested in logic at all.

But logic is very relevant to "being logical/reasonable", and seeing how mathematicians apply logic in their proofs is very relevant, and a starting point for more complex applications. I see mathematics as the simplest kind of application of logic you can have if you use only your brain for thinking, and not also a computer.

"Being logical/reasonable" also contains a big chunk of intuition/experience, and that is where machine learning will make a big difference.

Re: AlphaProof's Greatest Hits

#98

Post by youoy »

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

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 mathematics, but not Human level mathematics, in the same way that we can get LLM level films (something like Avengers, or the final season of GoT), but we are not going to get Human level films.

I suspect that there are no general level mathematics without the geometric experience of humans, so for general level mathematics one has to go through perceptions and interactions with reality first. In that case, general mathematics is one level over "laying bricks or cutting hair", so more complex. And the paradox is only a paradox for superficial reasoning.

Re: AlphaProof's Greatest Hits

#99

Post by chompychop »

Is it currently possible to reliably limit the cut-off knowledge of an LLM (either during training or inference)? An interesting experiment would be to feed an LLM mathematical knowledge only up to the year of proving a theorem, and then see if it can actually come up with the novel techniques used in the proof. For example, having only access to papers prior to 1993, can an LLM come up with Wiles' proof of FLT?

Re: AlphaProof's Greatest Hits

#100

Post by chvid »

samweb3 wrote: post #63
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.

I am building Memelang (memelang.net) to help with this as well. I'd love your thoughts if you have a moment!

Maybe include a section titled 'how is this different from and how is it related to' ie. relational algebra?
Post reply on HN