Beginners in computer science need to understand that there's no such thing as a computer programming method or discipline that "blocks AI mistakes via proof." This is not a position or opinion, it is a fundamental constraint called the "Halting Problem," originally identified by Alan Turing in 1936.
What applies to computer programming also applies to AI, for a reason that should be obvious. Lean, a widely used theorem prover, its everyday description notwithstanding, is Turing-complete and is therefore subject to the Halting Problem as well.
This is not meant to disparage one person's project. It is meant to identify a limit that applies to all such projects.
What applies to computer programming also applies to AI, for a reason that should be obvious. Lean, a widely used theorem prover, its everyday description notwithstanding, is Turing-complete and is therefore subject to the Halting Problem as well.
This is not meant to disparage one person's project. It is meant to identify a limit that applies to all such projects.