Merge branch 'main' of https://github.com/leanprover-community/con-nf

README.md

@@ -9,6 +9,7 @@ In this repository, we use the interactive theorem prover Lean to verify the dif
 The proof is now complete, and the theorem statements can be found in `ConNF/Model/Result.lean` ([source](https://github.com/leanprover-community/con-nf/blob/main/ConNF/Model/Result.lean), [docs](https://leanprover-community.github.io/con-nf/doc/ConNF/Model/Result.html)).
 
 See [our website](https://leanprover-community.github.io/con-nf/) for more information, the [documentation of our Lean code](https://leanprover-community.github.io/con-nf/doc/), and the [deformalisation paper](https://zeramorphic.github.io/con-nf-paper/main.l.pdf) that translates the Lean definitions into English.
+You can also read the [blueprint](https://leanprover-community.github.io/con-nf/blueprint/) that contains a human-readable version of the proof following the Lean code, with links to the formalisations of each statement.
 
 To run our code locally, install [elan](https://github.com/leanprover/elan), clone the repository, and run the following command in a terminal in the repository's root directory.
 ```

docs/index.md

@@ -12,6 +12,7 @@ In this repository, we use the interactive theorem prover Lean to verify the dif
 The proof is now complete, and the theorem statements can be found in `ConNF/Model/Result.lean` ([source](https://github.com/leanprover-community/con-nf/blob/main/ConNF/Model/Result.lean), [docs](https://leanprover-community.github.io/con-nf/doc/ConNF/Model/Result.html)).
 
 See [our website](https://leanprover-community.github.io/con-nf/) for more information, the [documentation of our Lean code](https://leanprover-community.github.io/con-nf/doc/), and the [deformalisation paper](https://zeramorphic.github.io/con-nf-paper/main.l.pdf) that translates the Lean definitions into English.
+You can also read the [blueprint](https://leanprover-community.github.io/con-nf/blueprint/) that contains a human-readable version of the proof following the Lean code, with links to the formalisations of each statement.
 
 To run our code locally, install [elan](https://github.com/leanprover/elan), clone the repository, and run the following command in a terminal in the repository's root directory.
 ```