I have formally defined 29 of 2529 baseline valsi. A table containing detailed statistics is available [0]. A full listing of theorems is available, with a table of contents [1]. The Metamath proof system is used to establish certainty in correctness from a minimum of axioms.
The next milestone is either formalizing 10% of baseline valsi, or proving a variant of {lo broda ku broda}. I currently project that about 40% of valsi can be formalized.
I welcome contributions. There are many theorems that can be transcribed from other sources of intuitionistic and relational logic, as well as folk theorems about Lojban which have not been formalized. There are also theorems which have been transcribed and informally justified but not yet formally proven.
I also welcome mathboxes [2] from community members who wish to use my existing work as a starting foundation for their own flavors of formal Lojban.
mi'e la korvo .i di'ai