This repository represents a formalization of Jürg Kohlas' Information Algebra text in Lean4.
The work has also kind of bled out into Shafer and Shenoy's Local Computation in Hypertrees which is rich and from which Kohlas' text draws a lot of its concrete foundations.
It is an opportunity to learn about both formalization in Lean4 and about the contents of the texts.
This is a work-in-progress; right now I'm still on Chapter 2 in both Kohlas and Shafer and Shenoy.