Terence Tao: preference

Transcript context

…You posted recently that it would be helpful to have a formal or semi-formal language for mathematical strategies as opposed to just mathematical proofs, which is what Lean specializes in. I would love to learn more about what that would involve or look like. We don’t really know. We’ve been very lucky in mathematics that we have worked out the laws of logic and mathematics, but this is a fairly recent accomplishment. It was started by Euclid two millennia ago, but only in the early 20th century did we finally list out the axioms of mathematics, the standard axioms of what we call ZFC, the axioms of first-order logic, and what a proof is. This we’ve managed to automate and have a formal language for. There could be some way to assess plausibility. You have a conjecture that something is true, you test a few examples, and it works out. How does this increase your confidence that the conjecture is true? We have a few sort of mathematical ways to model this, like Bayesian probability, for example. But you often have to set certain base assumptions, and there’s a lot of subjectivity still in these tasks. 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… 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 is plausible or not. If there was some semi-formal framework where this could be done semi-automatically in a way that isn’t easily hackable... It’s really important with these formal proof assistants that there are no backdoors or exploits you can use to somehow get your certified proof without actually proving it, because reinforcement learning is just so good at finding these backdoors. If there’s some framework that mimics how scientists talk to each other in a semi-formal way, using data and argument, but also constructing narratives... There’s some subjective aspect of science that we don’t know how to capture in a way that we can insert AI into it in any useful way. This is a future problem. There are research efforts to try to create automated conjectures, and maybe there are ways to benchmark these and simulate this, but it’s all very new science. Can you help me get some intuition? I have two sub-questions. One, it would be very helpful to have a specific example of what something like this would look like, the way scientists communicate that we can’t formalize yet. Two, it seems almost definitionally paradoxical to say you’re building up some narrative or natural language explanation and then also having something which you could have formalized. I’m sure there’s some intuition behind where that overlap is, and I’d love to understand that better.…

Stored transcript either side of the excerpt. The highlighted words are the published quote; the surrounding text is unedited source, never generated.