Hacker News Reader

Comment by mikmoila | Hacker News Reader

"The effort succeeded when we switched to using Prove2Me, an open collaborative platform for formalizing mathematics designed by Tianyi Peng and his collaborators at Columbia University."

So in the end, it required tooling crafted by humans.

View on HN

I was involved in building https://prove2.me (but I am not affiliated with Anthropic nor involved in anything related to FLT). I think the key insight in prove2me is to prove theorems "top-down", which allows a large number of users to collaboratively work on a single theorem statement. This setup also seems to work well for a "swarm" of agents. I posted more of my thoughts on the Lean Zulip.

There's nothing about prove2me that couldn't have been coded just like any other huge coding project frontier models have proven themselves extremely good at doing. It just happened to have been made by humans.

By this standard, no computer has ever accomplished anything, because humans built the computer. AI bubble about to burst any second now.

Humans built the tool which enabled the result. AI used the tooling for eliminating the dead ends. Yes, I can appreciate the practical value of all this, but IMHO it is not a kind of breakthrough result the article gives impression of.

A literal rock we carved patterns on and shot lightning into has accomplished something no human has.

How much more magical do you want this to be?

Tool or not it did something you could never have accomplished.

"you could never have accomplished"; I am not able to follow the logic here - there is no "magic" in LLMs, they're built by humans and we know what they do.

We don't know what they do. We shape them, but our understanding of how they get to their result is comparatively minimal.

I think you're referring to the fact that the sheer amount of computations is something too time consuming for us to follow? But still it is not "magical" - in theory we could follow all the steps, there's no hidden information.

No, I mean we just don't know what's going on in the circuits of the model at any substantial level. We set their architecture (hyperparameters), we pump them full of data (pretraining), and we shape how they behave through examples (SFT) and reward (RL), but we can't say with any certainty what the resulting model does internally.

You can scroll through https://transformer-circuits.pub/ to see the ~extent of our current understanding.

Yes "at any substancial level" . But still, its all about deterministic processes and still it obeys the law that the same input gives the same output. Or do you mean that the fluctuations like computing environment might ruin the determinism?

100% not deterministic at the scale they run.

Sure? I mean the internet is just a bunch of wires and some networking code not magic but at the same completely life alteringly magical.

My logic is that you personally could never have accomplished this feat with all the non LLM tools and content in the world. These kinds of things imply these methods are stepping beyond human ability.

Sure we put walls around it and optimize but the interior of that optimization is not something we understand.

You now have access to a system that for a price could solve something you simply are unable to solve. Not something we programmed it to solve, something that has never been solved before.

Nobody gave it an example of this proof, that's magical.

For now. That, too, will change in the future.

Same thing was said about cryptocurrency for like 15 years: "_in the future_ it will replace all fiat currency".

AI ≠ crypto.

Reply on news.ycombinator.com