These receive a formal proof as input, and each step is checked by direct application of a rule in the logic. No assistance is given to produce this formal proof in the first place, the user is expected to provide this as input.
The first system designed to check mathematical proofs with a computer was N.G. de Bruijn's Automath [19] implemented by Zandleven, which was used by Jutting [56] to to verify an encoding of Landau's Grundlagen der Analysis [29]. This was the only large mathematical text ever verified in the system.
The Mizar project [39,57] is attempting to build a library of formally verified mathematics (using software to perform this verification), large enough to be useful in the case where a proof is disputed. In this situation, the proponents of the proof simply need to encode the proof in the formal language recognised by the Mizar verification tools, which would then verify each step of the proof, assuming nothing but a set of agreed upon axioms. The Mizar Mathematical Library (MML) is a central repository of articles (proofs written in the Mizar language and verified with the Mizar software) constantly being added to. As this grows, it becomes easier to prove more complex theorems.
|
|
|