Questions about Fitch tableaux in mmb, lean.mm1

[Meta Kunt]

­So here are some questions I have.
I recently started getting interested in mm0 and I am quite impressed by the progress you have done. I'd like to build fitch tables and extract them from mmb files.
I didn't explore the code in detail but I read the first part of the complete specification. As I understand there are two streams in mmb and one simulates the stack of provable assertions inside the context.
My goal is to contribute to lean.mm1 first and hopefully extract it to metamath. But I'm not sure that this export to metamath will work.

Also it appears that Quot.ind is missing, can this one be proven via Quot.lift in some way? Also the prelude contains a bunch of nonsense from my point of view, I don't really see the point in defeq arrays, State monad, Strings/Chars or Syntax. From my point of view just defining the axioms, Lists, Nats and Options and the basic arithmetic functions on Nats and some on lists would be enough. I'd like to decomputify the lean4 proofs and remove nonmathematical context from them.

I'd be happy if I could write a tactic framework that is a bit nicer to look at. I'm afraid I don't really understand mm1 proofs. Maybe something that resembles the metamath or lean4 frontend would be nicer.
Longer term goal would be to convert mathlib into mm0/mm1/mmb and build fitch tables and complexity metrics. I've seen that you have planned to work on that on Zulip 

---

eclipso Mail Europe. Your E-Mail. Your Cloud. Your Office.