Agree to Disagree
This repository contains lean files relevant to We Can't Agree to Disagree, Formally: Aumann's Theorem and Assumption Accounting in Lean.
The formal proofs provided in this work were developed and verified using Lean 4.28.0. Compatibility with earlier or later versions is not guaranteed due to the evolving nature of the Lean 4 compiler and its core libraries.
Files
The folders input and output contain the inputs given to and outputs of AxiomProver for the two theorems;
the folder AgreeToDisagree contains the final hand-cleaned formalisation of Aumann's agreement theorem presented in the paper,
as well as another copy of AxiomProver's output for the
License
This repository uses the MIT License. See LICENSE for details.