mattr03

There's a project called lean4lean that implements lean in lean. I guess ideally, if you had a kernel optimisation idea you could do a copy of the Lean model lean4lean has created, add the optimisation, then prove your new lean is equivalent in terms of what it can prove to the old lean

yes and it has for a very long time. Stockfish took the neural net approach after AlphaZero showed it was a good idea as all modern chess engines have