There is a serious danger, which has nothing to do with bugs in Lean, which is a known problem for software verification and also applies in math: one must read the conclusions carefully to make sure that the right thing is actually proved.
I read Wilshaw's final conclusions carefully, and she did indeed prove what needed to be proved.
Every definition and theorem in mathlib and this project have been checked by Lean’s trusted kernel, which computationally verifies that the proofs we have constructed are indeed correct. However, Lean cannot check that the statements of the definitions and theorems match their intended English equivalents, so when drawing conclusions from the code in this project, translation to and from English must be done with care.
LLMs can write better English, but the curating step is still critical, because it also produces a lot of garbage.
Remember, we're not talking about a static target here, and the post I replied to set no qualifications on the claim that a human will always be needed to check that a mathematical definitions in the proof match the English equivalents. That's a long timeline on a rapidly moving target that is, as I said, already seems to be better than most humans at understanding and writing English.
Depends on the complexity, but for the simpler things I think I could get confident in a day or so. For more complex things, it might take longer to assess their ability.
But I'm not going to trust LLM blindly for anything.
> I replied to set no qualifications on the claim that a human will always be needed to check that a mathematical definitions in the proof match the English equivalents.
I don't defend this strong claim and limit my answer to LLMs (and mostly just state of the art). OTOH I believe that trust will continue to be a big topic for any future AI tech.
Again, what does "blindly" mean? Suppose you went a month without finding a single issue. Or two months. Or a year. The probability of failure must literally be zero before you rely on it without checking? Are you applying the same low probability failure on the human equivalent? Does a zero probability of failure for a human really seem plausible?
Choosing to handle it yourself does not reduce probability of error to zero, but it does move the locus of consequence when errors occur. "you have nobody to blame but yourself".
One reason people might trust humans over AI regardless of failure rate is answering the questions "what recourse do I have when there is an error" compounded by "is the error model self-correcting": EG when an error occurs, does some of the negative consequence serve to correct the cause of the error or doesn't it.
With another human in the loop, their participation in the project or their personal honor or some property can be jeopardized by any error they are responsible for. On the one hand this shields the delegator from some of the consequence because if the project hemorrhages with errors they can naturally demote or replace the assistant with another who might not have as many errors. But on the other hand, the human is incentivized to learn from their mistakes and avoid future errors so the system includes some self-correction.
Using a static inference LLM, the user has little recourse when there is an error. Nowhere to shift the blame, probably can't sue OpenAI over losses or anything like that. Hard to replace an LLM doing a bad job aside from perhaps looking at ways to re-fine-tune it, or choose a different model which there aren't a lot of materially competing examples.
But the biggest challenge is that "zero self-correction" avenue. A static-inference LLM isn't going to "learn from its mistakes", and the same input + random seed will always produce the same output. The same input with a randomized seed will always produce the same statistical likelihood of any given erroneous output.
You'd have to keep the LLM on a constant RLHF fine tuning treadmill in order for it to actually learn from errors it might make, and then that re-opens the can of worms of catastrophic forgetting and the like.
But most importantly, that's not the product that is presently being packaged one way or the other and no company can offer any "learning" option to a single client at an affordable price that doesn't also commoditize all data used for that learning.
If the LLM required a constant fine-tuning treadmill, you wouldn't actually use it in this application. You could tell if you were on such a treadmill because its error rate wouldn't be improving fast enough in the initial phases while you were still checking its work.
As for what recourse you have in case of error, that's what fine-tuning is for. Your recourse is you change the fine-tuning to better handle the errors, just like you would correct a human employee.
Employees are not financially liable for mistakes they make either, just their job is at stake, but this is all beside the point, at the end of the day the only rational question is: if the LLM's error rate is equal to or lower than a human employee, why prefer the human?
till they incorporate more of what some of your writing and loose their advantages
Imagine someone saying "just write good English lol eventually you can do good math". I'm aware you're not quite saying this but you seem really distracted by the human language representation of math, connecting doing math proofs to generating English sentences from some probability distribution is ridiculous. Of course it is possible LLMs can do math, if it's matter of having nonzero chance, there's also a nonzero chance we are all brains in vats. More rationally if someone says something is possible they should produce some evidence that it is possible. And then we decide whether that evidence is good enough.
Writing well in any human language is not good enough, since it is entirely different from being able to tell whether a set of formal axioms capture certain ideas about a mathematical structure. This is a model theoretic issue. Neural network theorem provers deal with proof theoretic issue.
The best LLM-Lean provers right now are tackling the very challenging problem of how to generate the right sequence of tactics for infinite search space, all relying on, excuse me, undergrad students to formalize proofs and statements for them.
Wilshaw's formalization is not vulnerable to this objection, though libraries were used. What is proved is that a certain defined concept satisfies a certain suite of formulas of first order logic. If there is a predicate satisfying that suite of formulas, NF is consistent.
human interaction helps create confidence. But the software is extremely reliable: a philosophical challenge based on bugs in theorem proving software just is not going to hold water.
[1]: https://inutile.club/estatis/falso/
[2]: https://www.youtube.com/watch?v=sv97pXplxf0
[3]: https://terrytao.wordpress.com/2023/11/18/formalizing-the-pr...
The trusted codebase becomes that checking algorithm, along with the "compiler" that translates the high-level language to term rewriting syntax. Formally verifying that codebase is a rather circular proposition (so to speak), but you could probably bootstrap your way to it from equations on a chalkboard.
From a foundational perspective, it is also important to note that this proof is one of equiconsistency between NF and the Lean kernel, which itself is handchecked. Mechanized theorem provers preserve that level of correctness imputed to them via outside injection, from humans or other out-of-band systems.
They do exactly what you tell them to.