Expertise and information: an epistemic logic perspective

This repository contains the LaTeX source for the paper, the appendix (containing missing proofs), and formalisation of some of the proofs in Lean.

• Paper
• Appendix

The proofs were checked with Lean version 3.35.1. To build, set up leanproject and run leanproject get-mathlib-cache followed by leanproject build, from the lean directory.

The following results/definitions have been formalised (links go to the relevant section of the source code):

• Definition 1
• Proposition 2
• Definition 2
• Definition 3
• Lemma 2
• Lemma 3: 1, 2, 3
• Theorem 3
• Lemma 4
• Lemma 5: 1, 2, 3, 4
• Lemma 6
• Lemma 7: 1, 2, 3
• Lemma 8: 1, 2, 3
• Corollary 1: 1, 2
• Lemma 9
• Theorem 4
• Proposition 4
• Lemma 10
• Proposition 6
• Theorem 8

This list is automatically generated from the Lean/LaTeX source by the scripts in the python directory.