Short answer: Jordan Metzner's leaderboard gave Gemini 98 and ChatGPT 70. Carina notes one model proved it for natural numbers instead of integers, and says compiling the Lean proof should be more painless than an LLM judge.
Watch this answer from Episode 22 (starts at 5:27) · Episode 22 notes and transcript
From Episode 22: Let's do the Math!, starting at 5:27.
Carina [5:27]: Let's do Fermat Little Theorem.
Jordan Metzner [5:29]: Okay. Fantastic. So that's considered an intermediate problem here. And here's the problem. For a prime number, p in any integer, a non divisible by p, we have a to the p minus one equals one mod p
Carina [5:41]: That's right.
Jordan Metzner [5:42]: Provide a formal proof in Lean four syntax. So I just read that out loud just for the audience, you know. So first, let's roast the LLMs. So now we'll have the LLMs. This is gonna take a little bit longer, so we can maybe chat in the meantime.
Carina [5:53]: It's fascinating. There are so many Fermat theorems. I think like when I selected it, I was actually having something else in mind. But yes, I think this one is the Fermat little theorem.
Jordan Metzner [6:01]: But ChatGPT told me that it is when I built the app. So as I vibe coded this thing, I'm pretty sure it is. But the good part is is that you can kind of submit, whatever formula you want. What I tried to do is get a collection of about 10 problems of different difficulty so that it could test the application and see kind of For some how well it does. The easiest one was Pythagorean theorem, then I felt like, that's even like too difficult just to check, basis of truth. That's why I built the Okay. Mathematic one. Just to check, if everything's working essentially.
Carina [6:31]: Yeah. And that's for lean? So it's generating all
Jordan Metzner [6:34]: Yeah. It's gonna generate lean response. Wow. -huh. Yeah.
Carina [6:36]: Yeah. Yeah. We're not seeing the lean.
Jordan Metzner [6:37]: Okay. Cool. Alright. So here we go. So here's Gemini Here's the response. Here's the theorem. Here it just gives the oh, here we'll provide both versions of Lean. Okay? Here's GPT five.
Carina [6:50]: No. That is Lean. I haven't seen Lean in the Gemini Pro one yet. If you scroll down, the first one.
Jordan Metzner [6:58]: It says it's below. Let's keep going. Right here.
Carina [7:00]: Yeah. Got
Jordan Metzner [7:00]: It. Right here. Cool. Alright. So we got import Mathlib. Right? So we've got like these different ones. What we can do, first, we can compare the results. So we can just review them all side by side. And then we can judge the proofs. I think that's the way to do it. We have two ways to do it, actually. This should score it. Yeah. So then it'll judge all the proofs. Mhmm.
Carina [7:20]: We could also, right, like take that lean proof and then put it in like lean land and like, and see if it compiles, which should be hopefully be pain more painless than having LLM judge. Yeah.
Jordan Metzner [7:34]: Sure. So we can take like I don't know which answer we want as
Carina [7:37]: Probably wouldn't want to take the lean you know, just start with import Mathlib.
Jordan Metzner [7:41]: Yeah. Yeah. I got it. I But I'm saying we could just pick which one of these answers we want and we can go into a lean editor.
Carina [7:48]: Entire thing? Yeah.
Jordan Metzner [7:49]: Yeah. Okay. Let's just let the judging finish and let's see how well that does. It's just a really cool way to compare any type of multi level LLM results against any dataset. Right? And like in this case, I chose lean and math. But, know, this could be a lawyer writing a contract and sending it out, amongst all four and asking them all to bring back, which contract is the best. So it could be applicable in many businesses, even ones that are outside the scope of mathematics. Fascinating. Cool. So I have a leaderboard. It gave Gemini the best score. ChatGPT is 70, and so on and so forth.
Carina [8:22]: So That that's weird. Don't you think? For two, it says it proves the theorem for natural numbers instead of for integers. Oh, I guess oh, it just didn't go with the negative numbers. That's fascinating. Just a close miss. Gemini is 98. Wow. Okay. It's great.
Jordan Metzner [8:40]: So I think what would be really interesting, Carina, would be is in this type of problem set would be to get like thousands. Right? And just iterate this over and over again and find out where these models truly fail. And if you do this at enough iterations, like, I don't know what, like, the right end number would be. But my guess is for each, like, major type of problem set, you'd be able to find the model's weakness pretty quickly and its ability to resolve those types of problems.
Carina [9:06]: And that's actually the first thing we did when the office is, still camper chairs and plastic foldable table. It's what we did.
Jordan Metzner [9:15]: That's awesome. Okay. So anyway, that's my math roaster. I hope you like it. It's great. And that's enough about me. Let's jump into Axiom.
Carina [9:24]: That was super cool.
