Envelope-to: lojban-list-archive@lojban.org
Delivery-date: Sun, 13 Aug 2023 23:45:31 -0700
Sender: lojban@googlegroups.com
Date: Sun, 13 Aug 2023 23:45:22 -0700 (PDT)
From: "gleki.is...@gmail.com" <gleki.is.my.name@gmail.com>
To: lojban <lojban@googlegroups.com>
Message-Id: <25be0bf4-d213-4a35-8bd4-e82cf4104b70n@googlegroups.com>
In-Reply-To: <f3d0d528-a9bf-43bc-bc02-f4d981c19f7dn@googlegroups.com>
References: <f3d0d528-a9bf-43bc-bc02-f4d981c19f7dn@googlegroups.com>
Subject: [lojban] Re: Baseline Lojban is 1% formalized
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_20520_371493676.1691995522368"
Reply-To: lojban@googlegroups.com
Precedence: list
Mailing-list: list lojban@googlegroups.com; contact lojban+owners@googlegroups.com
X-Spam_score: -7.6
X-Spam_score_int: -75
X-Spam_bar: -------

------=_Part_20520_371493676.1691995522368
Content-Type: multipart/alternative; 
	boundary="----=_Part_20521_1797627867.1691995522368"

------=_Part_20521_1797627867.1691995522368
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

banli ki'e

On Tuesday, August 1, 2023 at 8:08:38=E2=80=AFPM UTC+2 mostawe...@gmail.com=
 wrote:

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

--=20
You received this message because you are subscribed to the Google Groups "=
lojban" group.
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to lojban+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/=
lojban/25be0bf4-d213-4a35-8bd4-e82cf4104b70n%40googlegroups.com.

------=_Part_20521_1797627867.1691995522368
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

banli ki'e<br /><br /><div class=3D"gmail_quote"><div dir=3D"auto" class=3D=
"gmail_attr">On Tuesday, August 1, 2023 at 8:08:38=E2=80=AFPM UTC+2 mostawe=
...@gmail.com wrote:<br/></div><blockquote class=3D"gmail_quote" style=3D"m=
argin: 0 0 0 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left=
: 1ex;"><div>I have formally defined 29 of 2529 baseline valsi. A table con=
taining 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.<br></div><=
div><br></div><div>The next milestone is either formalizing 10% of baseline=
 valsi, or proving a variant of {lo broda ku broda}. I currently project th=
at about 40% of valsi can be formalized.</div><div><br></div><div>I welcome=
 contributions. There are many theorems that can be transcribed from other =
sources of intuitionistic and relational logic, as well as folk theorems ab=
out Lojban which have not been formalized. There are also theorems which ha=
ve been transcribed and informally justified but not yet formally proven.<b=
r></div><div><br></div><div>I also welcome mathboxes [2] from community mem=
bers who wish to use my existing work as a starting foundation for their ow=
n flavors of formal Lojban.<br></div><div><br></div><div>mi&#39;e la korvo =
.i di&#39;ai<br></div><div><br></div><div>[0] <a href=3D"https://mostawesom=
edude.github.io/brismu/index.html" target=3D"_blank" rel=3D"nofollow" data-=
saferedirecturl=3D"https://www.google.com/url?hl=3Den&amp;q=3Dhttps://mosta=
wesomedude.github.io/brismu/index.html&amp;source=3Dgmail&amp;ust=3D1692081=
910474000&amp;usg=3DAOvVaw001CTO0caCkdfyqsUL3auw">https://mostawesomedude.g=
ithub.io/brismu/index.html</a></div><div>[1] <a href=3D"https://mostawesome=
dude.github.io/brismu/mmtheorems.html" target=3D"_blank" rel=3D"nofollow" d=
ata-saferedirecturl=3D"https://www.google.com/url?hl=3Den&amp;q=3Dhttps://m=
ostawesomedude.github.io/brismu/mmtheorems.html&amp;source=3Dgmail&amp;ust=
=3D1692081910474000&amp;usg=3DAOvVaw3T6NPpfZ0uIqPpN9WH5lCB">https://mostawe=
somedude.github.io/brismu/mmtheorems.html</a></div><div>[2] <a href=3D"http=
s://us.metamath.org/ileuni/mathbox.html" target=3D"_blank" rel=3D"nofollow"=
 data-saferedirecturl=3D"https://www.google.com/url?hl=3Den&amp;q=3Dhttps:/=
/us.metamath.org/ileuni/mathbox.html&amp;source=3Dgmail&amp;ust=3D169208191=
0474000&amp;usg=3DAOvVaw0aNcxk8jdyIKbi_Bz1Q06l">https://us.metamath.org/ile=
uni/mathbox.html</a></div></blockquote></div>

<p></p>

-- <br />
You received this message because you are subscribed to the Google Groups &=
quot;lojban&quot; group.<br />
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to <a href=3D"mailto:lojban+unsubscribe@googlegroups.com">lojban+unsub=
scribe@googlegroups.com</a>.<br />
To view this discussion on the web visit <a href=3D"https://groups.google.c=
om/d/msgid/lojban/25be0bf4-d213-4a35-8bd4-e82cf4104b70n%40googlegroups.com?=
utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.com/d/msgid/l=
ojban/25be0bf4-d213-4a35-8bd4-e82cf4104b70n%40googlegroups.com</a>.<br />

------=_Part_20521_1797627867.1691995522368--

------=_Part_20520_371493676.1691995522368--