https://x.com/VictorTaelin/status/1811167900780175423
Can recommend taking a look at their recorded Twitch stream to see it in action.
Also, it's the most complicated pure reasoning task you can build. So working on theorem-proving AI may help in reasoning and reliability.
This can be applied on something like: Is your extension on distributed system protocol (like Paxos) correct? Does my novel security system hold certain properties? etc etc...
... basically when you need to be sure certain properties of your system hold.
You can verify only the critical parts, as in a data structure or algorithm, or you can verify higher-level parts of a system. All you're doing with math is thinking (out loud) and writing a proof is constructing a convincing argument. If you need to be certain that a thread doesn't leak addresses in shared memory to other threads then you ought to take the time to think through how you're going to achieve that and prove that your solution works.
10+ years out from a Finance PhD where I ended up using numerical methods because I really didn't have the math skills to prove closed form solutions.
Would love to know if, starting with a stochastic differential equation, how far your can go re: applying Ito's lemma and working through the math to get to a closed form solution (using Lean).
It the main advantage of Lean (ignoring LLM assistance) that you build up declarative code that, as you incrementally work on the proof, guarantees that the proof-so-far is correct?
So you're still "working through the math" but rather than un-executable math notation written on a pad, you have "by induction" a guaranteed valid argument up to the point you are at in the proof?
Just trying to build a mental model of Lean > pen and pad.
https://github.com/lecopivo/SciLean
To your last point, the idea is that numerical approximations can be introduced (and introduction will ask for proofs of validity! but you can ignore "the proving" via `sorry`) to go from un-executable math notation (in Lean4) to executable!
Whether the proof goes through doesn't affect the final executable.
Privately, I think Lean could be incredibly powerful if baked deep into an ML's kernel/structure/training process. I think an AI proof of something like the Riemann Hypothesis may well be possible if you get enough resources behind it.
I read the article. It doesn't say anything about generating new proofs to train on. It only mentions scraping Github for lean theorems+proofs.
Not sure of the feasibility of implementing lean as a GPU kernel, if you meant that. Also I'm not sure it makes sense to run Lean inside the (mostly matmul) training process. Now to use it to prepare some training data, it seems more realistic. But that seems to be what AlphaProof tries to do in the reinforcement step, if I'm not mistaken.
The problem is mostly that it's fairly intensive to code an efficient RL trainer for this, and even then it's expensive to run the training.
Still not convinced that LLMs do anything else than rearranging other people's work.
Effects can already be seen: The Washington Post used to display articles when found via Google, now you get a paywall. And I can no longer criticize them for it.
I’m not convinced that most people do anything else than rearrange other people’s work.
It's amazing how useful and powerful that is in certain contexts.
