I've never worked with Lean 4 before, but this project really caught my attention. The idea of using formal verification to explore cognitive theories and prove properties of memory and learning models is really interesting.
Maybe I will try it, if I will learn Lean 4 at sufficient level.
Do you need a good Lean 4 level for this project and what about vibecoding with your library?