Lean 4 artifact: request for external build + documentation

Stream: new members

[Bob Jefferson]

Can anyone assist? I’ve put together a Lean 4 library (archived on Zenodo) formalising a finite algebraic core for Dirichlet convolution and Möbius inversion, with a short companion paper describing the code.

I’m looking for one independent reader willing to check two things only:

1. the code builds cleanly from the archive, and

2. the paper accurately describes what the Lean code proves.

I’m not asking for endorsement of claims or interpretations — just a technical artifact check.

Thanks in advance.

https://doi.org/10.5281/zenodo.17922744