Vlad Tenev

I think the bet that

we're making with mathematical superintelligence with Aristotle is that these things actually have the same solution.

That solution is something called formal verification.

What formal verification is basically, you write a spec.

The spec is essentially you can think of as the list of properties and rules that your system has to follow.

and then you formally and mathematically prove that any code that you generate follows these rules and now formal verification existed before ai the french have deployed it like in in a lot of places like the paris train stations are formally verified and you can mathematically prove that the trains aren't going to hit each other and i think there's something like 30 years with no accidents but these are humans hand crafting

very artisanal work of just making sure that all of the mathematical properties are proved by hand.

So the bet that we're making is there's actually going to be a new paradigm of vibe coding and vibe proving where it's not just like the Wild West, but things are constrained.

by these theorems that you have to follow.

And if I think about harmonic, the sort of like North Star goal is to solve a Millennium Prize worthy problem.

So like one of the big problems of mathematics.

And I think that with a fairly high degree of confidence, these don't get solved very often.

The last one was about 20 years ago.

by this Russian guy, Grigory Perelman.

He solved the Poincaré conjecture.

I think the next one very likely will be either significant AI assist or maybe even largely solved by AI.

So that's kind of the long-term goal.

But of course, we have to break that down into

into shorter term goals.

And the first accomplishment we had was to get a gold medal or gold medal level performance at the International Math Olympiad, which is like the most prestigious math competition, but sort of high school level problems.