Difference between implementation and formalisation in a proof assistant

Question

Some authors refer to their works as "implementation of the theory in (let's say) Agda", some refer as "formalization of the theory in Agda". What is the difference between them?

Answer 1

To turn my comments into an answer: Typically one would talk about formalizing something which starts out as informal. So proof assistants are good at formalizing informal mathematical definitions and proofs. For example, a lot of recent work has gone into formalizing probability theory.

While it is possible to formalize something in a formal system using just pen and paper (as done in, for example, Principia Mathematica), it is more common now-a-days to formalize something on a computer. The computer can check that your formalization is correct, following the rules of the formal system. But to do that, one needs to implement the formal system. Various proof assistants implement formal systems/logics like (specific versions) of type theory or set theory.

Now as to the paper you mentioned in the comments, it seems to be a paper about a generalization of the univalence principle which can be stated in two-level type theory (2LTT)---itself a generalization of Martin-Löf type theory (MLTT). The paper is "informal" in that it doesn't give formal proofs or supply any computer code. The last sentence in the paper is:

The results presented here should be formalizable in a computer proof assistant implementing 2LTT.

I think the authors are just stating that one can formally write all the definitions and proofs in the paper in a proof assistant based on two-level type theory, if such a proof assistant exists. But since it likely doesn't exist yet, one has to implement 2LTT in some computer proof assistant first. (This is similar to how Vodvosky formalized the univalence axiom and it's consequences in Coq, which implements a variant of MLTT.) (Note: This likely only makes sense since all the theorems in the paper are positive, namely theorems of the form: "In 2LTT the following holds: ...". If on the other hand, there was a meta-theorem of the form "The following can't be proved in 2LTT: ...", then that wouldn't be formalizable in 2LTT because of Gödel's theorem.)

Now, as for the github repo, I see your confusion since they call it a "Lean Formalisation of Two-Level Type Theory", but also describe the file fibrant.lean as an "implementation of the two-level type theory ". Here is what I think is going on. Lean 2 (unlike Lean 3 and 4) has support for homotopy type theory (HoTT) built in. You could say (the HoTT version of) Lean 2 is an implementation of HoTT. I don't know much about 2LTT, but it looks like to implement it o ntop of Lean 2, the repo authors didn't need to change the underlying kernel of Lean 2 which implements type theory. Instead they just have to add in some additional axioms and definitions. (You can see the axioms by looking for keyword constant in the file fibrant.lean.) So they are doing the same kind of tasks as typical formalization work, namely adding a bunch of definitions, axioms, and proofs to Lean 2.