7 ms·

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

"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.

behnamoh 12d ago
For now. That, too, will change in the future.
- deepsun 12d ago
  Same thing was said about cryptocurrency for like 15 years: "_in the future_ it will replace all fiat currency".
  - behnamoh 12d ago
    AI ≠ crypto.
educasean 12d ago
By this standard, no computer has ever accomplished anything, because humans built the computer. AI bubble about to burst any second now.
- mikmoila 12d ago
  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.
  - johnsmith1840 12d ago
    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.
    - mikmoila 12d ago
      "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.
      - Philpax 12d ago
        We don't know what they do. We shape them, but our understanding of how they get to their result is comparatively minimal.
        mikmoila 12d ago
        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.
        Philpax 12d ago
        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/ https://transformer-circuits.pub/ to see the ~extent of our current understanding.
        mikmoila 12d ago
        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?
        johnsmith1840 12d ago
logicprog 12d ago
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.
marwahaha 12d ago
I was involved in building https://prove2.me 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.

behnamoh 12d ago

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

deepsun 12d ago
Same thing was said about cryptocurrency for like 15 years: "_in the future_ it will replace all fiat currency".
- behnamoh 12d ago
  AI ≠ crypto.

educasean 12d ago

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

mikmoila 12d ago
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.
- johnsmith1840 12d ago
  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.
  - mikmoila 12d ago
    "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.
    - Philpax 12d ago
      We don't know what they do. We shape them, but our understanding of how they get to their result is comparatively minimal.
      - mikmoila 12d ago
        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.
        Philpax 12d ago
        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/ https://transformer-circuits.pub/ to see the ~extent of our current understanding.
        mikmoila 12d ago
        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?
        johnsmith1840 12d ago

logicprog 12d ago

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.

marwahaha 12d ago

I was involved in building https://prove2.me 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.