PierreSenellartprovenance

Lean4 formalization of some provenance notions

Lean4 formalization of some provenance notions

Continuous Integration

This repository includes some Lean4 formal definitions and proofs relevant for provenance in databases. One of the goal of this project is to provide a formal semantics to the operations performed in the provenance-aware relational database extension ProvSQL. This also complements the description of the data model of ProvSQL provided in Sen, Maniu & Senellart, "ProvSQL: A General System for Keeping Track of the Provenance and Probability of Data", ICDE 2026.

Full documentation is available at https://provsql.org/lean-docs/Provenance.html.

License

These formal definitions and proofs are provided as open-source software under the MIT License. See LICENSE.

Contact

https://github.com/PierreSenellart/provenance-lean

Pierre Senellart pierre@senellart.com

Bug reports and feature requests are preferably sent through the Issues feature of GitHub.