News from the research group Knowledge-Based Systems of January 20, 2025

ICCL Researchers Contribute to Lean Standard Library

Johannes Tantow (former student at the Knowledge-Based Systems group; now Research Associate at TU Chemnitz) and Lukas Gerlach (Research Associate at the Knowledge-Based Systems group) have recently contributed a sizable number of results around hash maps to the standard library of the interactive theorem prover Lean. Interactive theorem provers allow to write proofs in a machine-verifiable format. In the case of Lean, proofs are written as part of a functional programming language.

In his Diploma Thesis, Johannes, under supervision of Lukas, Stephan Mennicke, and Markus Krötzsch, built a tool that is able to check correctness of Datalog proof trees. This tool is written and formally verified in Lean. That is, if the tool accepts a given Datalog proof tree, we can be certain that the proof tree is indeed correct. For performance reasons, this tool is using hash map data structures, which already existed in the Lean standard library but only a handful of correctness results had been formalized at the time. For example, one would like to verify that if a hash map is built from a list of key-value pairs, then each of the keys occurs in the hash map afterwards. While such results seem obvious, it is a non-trivial task to prove this over the internal implementation of the hash map.

In close collaboration with members of the Lean development team, Johannes and Lukas spent some time throughout the last weeks and months to fill in some of these gaps. A PR verifying properties around building hash maps from lists just landed on the main branch with around 5000 lines of code added. These changes will be part of the upcoming Lean version 4.17 and be used by Johannes and Lukas themselves to round up the already existing Datalog proof tree verification tool.

Both Johannes and Lukas are very happy with how the collaboration went. "It was a great opportunity to not only make some tangible contributions for the Lean community but also to obtain valuable insights about developing Lean at scale", Lukas said.