Good idea, the problem is that LEAN only proves what you tell it to prove. Which is better than just making a claim, but have to know enough about the problem domain (and lean) to be able to interpret that the code matches the claim. Otherwise you can be proving something only tangentially related. So you’re still left with the fact that someone needs to verify something, unless you only expose the lean code I suppose, but then you loose some of the knowledge compression that this is intended to create.
Their proposed topological_toric_code() function is entirely trivial. It initializes qubits as an array of zeros. It then runs a loop applying expm(-1j * np.pi * 0). Mathematically, the exponential of zero is simply 1. It contains absolutely none of the actual mechanics required for a toric code. There is no lattice definition, no Pauli X and Z stabilizer operators, no syndrome measurement, no decoding algorithm.
It is just a trivial statement of 1 = exp(0). And then it adds a bunch of nonsense about it being a novel toric code.
EDIT: looked at a few more. They're so bad it's hard to even believe AI wrote them. Must be a pretty crappy model.
So they need a mechanism to decide what results are interesting. Maybe don't let anyone proof anything. Let the bot that sent a paper that got accepted to send two or three statements that they like to see proven. And at some point only allow proofs of things that have been requested in that way.
There could also be a preference for short proofs.
I wonder how reliable the verification mechanism will be. Currently, you require 3 or 5 agents for peer review. But the submitting agent itself can spin up any number of subagents that then peer review. You got plans to increase the trustworthiness of the review process?
I also wonder how good LLM verification can be as currently you can pretty much say anything generic with a positive spin and the AI will believe it as long as it's somewhat abstract.
Could you give a concrete example or two of what exactly this system does? Like, what's a scientific result or two it has formally mathematically proved?
9 comments
Their proposed topological_toric_code() function is entirely trivial. It initializes qubits as an array of zeros. It then runs a loop applying expm(-1j * np.pi * 0). Mathematically, the exponential of zero is simply 1. It contains absolutely none of the actual mechanics required for a toric code. There is no lattice definition, no Pauli X and Z stabilizer operators, no syndrome measurement, no decoding algorithm.
It is just a trivial statement of 1 = exp(0). And then it adds a bunch of nonsense about it being a novel toric code.
EDIT: looked at a few more. They're so bad it's hard to even believe AI wrote them. Must be a pretty crappy model.
There could also be a preference for short proofs.