Terence Tao

I mean, we've been very lucky in mathematics that we have worked out the laws of logic and mathematics.

But this is actually a fairly recent accomplishment.

I mean, it was started by Euclid.

millennia ago, but only in the early 20th century did we finally list the axioms of mathematics, the standard axioms of ZFC, and the axioms of first-order logic, and this is what a proof is, and this we've managed to automate and have formal language for.

But

there could be some way to assess plausibility of certain, you know, so you have a conjecture that something is true, you test a few examples and it works out, like how does this increase your confidence that the conjecture is true?

We have a few sort of mathematical ways to model this, Bayesian probability, for example,

But you often have to set certain base assumptions and there's a lot of subjectivity still in these tasks.

It's not clear, I mean, this is more of a wish than a plan to develop these languages, but just seeing how successful having a formal framework in place like Lean has made deductive proofs so much easier to automate and train AI on.

If there was some similar framework, so the bottleneck for using AI to create strategies and make conjectures is we have to rely on human experts and the test of time to validate whether something's plausible or not.

If there was some semi-formal framework where this could be done

semi-automatically in a way that isn't sort of easily hackable.

Of course, it's really important with these formal proof assistance that there are just no backdoors or exploits that you can do to somehow get your certified proof without actually proving it because reinforcement learning is just so, so good at finding these backdoors.

Yeah, if a strong framework that sort of mimics how scientists talk to each other in a semi-formal way, you know, using data and argument, but also, you know, constructing narratives and there's some subjective aspect of science.

that we don't know how to capture in a way that we can insert AI into them in any useful way.

Interesting.

So yeah, this is a future problem.

I mean, there are research efforts to try to create automated conjectures and maybe there are ways to benchmark these and get some way to simulate this, but it's all very, very new science.

All right, so an example of a conjecture.

So Gauss was interested in the prime numbers, and he computed, he created one of the first mathematical data sets.