Baseline Lojban is 1% formalized

Sett 61 ganger
Hopp til første uleste melding

Corbin Simpson

ulest,
1. aug. 2023, 14:08:3801.08.2023
til lojban
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

gleki.is...@gmail.com

ulest,
14. aug. 2023, 02:45:2214.08.2023
til lojban
banli ki'e
Svar alle
Svar til forfatter
Videresend
0 nye meldinger