AgreeToDisagree

KO | EN

gitlite — search

#react #ai #typescript #android #machine-learning #linux #nodejs #cli #kubernetes #security #pytorch #ios #mcp #openai

AgreeToDisagree

(★ 22)

Lean formalizations of the paper "We Can't Agree to Disagree, Formally: Aumann's Theorem and Assumption Accounting in Lean"

AgreeToDisagree 최신버젼 다운로드

최종 버전 다운로드 (.zip)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

[![Logo for Axiom Math](https://raw.githubusercontent.com/AxiomMath/AgreeToDisagree/main/logo.svg)](https://axiommath.ai/)

# 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](https://papers.ssrn.com/sol3/papers.cfm?abstract_id=6837298).

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 $p$-belief version.

## License

This repository uses the MIT License. See [LICENSE](LICENSE) for details.

## Repository maintainers

- [Ruiz Chen](https://github.com/Ruizsolveall)
- [Ben Eltschig](https://github.com/peabrainiac)
- [Ken Ono](https://github.com/kenono691)
- [Jujian Zhang](https://github.com/jjaassoonn)

AgreeToDisagree

AgreeToDisagree 최신버젼 다운로드

오늘의 추천 프로젝트

Was this content helpful?

Recent Feedback

AgreeToDisagree

AgreeToDisagree 최신버젼 다운로드

오늘의 추천 프로젝트

Was this content helpful?

Recent Feedback

Download README