Also: https://github.com/jeffshrager/ExecutableArchaeology/tree/ma...

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?