Envelope-to: lojban-list-archive@lojban.org
Delivery-date: Tue, 01 Aug 2023 11:08:43 -0700
Sender: lojban@googlegroups.com
Date: Tue, 1 Aug 2023 11:08:37 -0700 (PDT)
From: Corbin Simpson <mostawesomedude@gmail.com>
To: lojban <lojban@googlegroups.com>
Message-Id: <f3d0d528-a9bf-43bc-bc02-f4d981c19f7dn@googlegroups.com>
Subject: [lojban] Baseline Lojban is 1% formalized
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_2650_421532160.1690913317946"
Reply-To: lojban@googlegroups.com
Precedence: list
Mailing-list: list lojban@googlegroups.com; contact lojban+owners@googlegroups.com
X-Spam_score: 0.1
X-Spam_score_int: 1
X-Spam_bar: /
X-Spam-Report: Spam detection software, running on the system "50bab00d4276",
 has NOT identified this incoming email as spam.  The original
 message has been attached to this so you can view it or label
 similar future email.  If you have any questions, see
 @@CONTACT_ADDRESS@@ for details.
 
 Content preview:  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 sy [...] 
 
 Content analysis details:   (0.1 points, 5.0 required)
 
  pts rule name              description
 ---- ---------------------- --------------------------------------------------
  0.0 URIBL_BLOCKED          ADMINISTRATOR NOTICE: The query to URIBL was
                             blocked.  See
                             http://wiki.apache.org/spamassassin/DnsBlocklists#dnsbl-block
                              for more information.
                             [URIs: metamath.org]
  0.8 BAYES_50               BODY: Bayes spam probability is 40 to 60%
                             [score: 0.5000]
 -0.0 RCVD_IN_DNSWL_NONE     RBL: Sender listed at https://www.dnswl.org/,
                              no trust
                             [209.85.160.59 listed in list.dnswl.org]
  0.0 RCVD_IN_MSPIKE_H3      RBL: Good reputation (+3)
                             [209.85.160.59 listed in wl.mailspike.net]
  0.2 HEADER_FROM_DIFFERENT_DOMAINS From and EnvelopeFrom 2nd level
                             mail domains are different
 -0.0 SPF_PASS               SPF: sender matches SPF record
  0.0 FREEMAIL_FROM          Sender email is commonly abused enduser mail
                             provider
                             [mostawesomedude[at]gmail.com]
  0.0 SPF_HELO_NONE          SPF: HELO does not publish an SPF Record
  0.0 HTML_MESSAGE           BODY: HTML included in message
 -0.1 DKIM_VALID             Message has at least one valid DKIM or DK signature
  0.1 DKIM_SIGNED            Message has a DKIM or DK signature, not necessarily
                             valid
 -0.1 DKIM_VALID_AU          Message has a valid DKIM or DK signature from
                             author's domain
 -0.1 DKIM_VALID_EF          Message has a valid DKIM or DK signature from
                             envelope-from domain
 -1.0 MAILING_LIST_MULTI     Multiple indicators imply a widely-seen list
                             manager
  0.2 FREEMAIL_FORGED_FROMDOMAIN 2nd level domains in From and
                             EnvelopeFrom freemail headers are
                             different
  0.0 RCVD_IN_MSPIKE_WL      Mailspike good senders

------=_Part_2650_421532160.1690913317946
Content-Type: multipart/alternative; 
	boundary="----=_Part_2651_1317818005.1690913317946"

------=_Part_2651_1317818005.1690913317946
Content-Type: text/plain; charset="UTF-8"

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

[0] https://mostawesomedude.github.io/brismu/index.html
[1] https://mostawesomedude.github.io/brismu/mmtheorems.html
[2] https://us.metamath.org/ileuni/mathbox.html

-- 
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 email to lojban+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/lojban/f3d0d528-a9bf-43bc-bc02-f4d981c19f7dn%40googlegroups.com.

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

<div>I have formally defined 29 of 2529 baseline valsi. A table containing =
detailed statistics is available [0]. A full listing of theorems is availab=
le, with a table of contents [1]. The Metamath proof system is used to esta=
blish certainty in correctness from a minimum of axioms.<br /></div><div><b=
r /></div><div>The next milestone is either formalizing 10% of baseline val=
si, or proving a variant of {lo broda ku broda}. I currently project that a=
bout 40% of valsi can be formalized.</div><div><br /></div><div>I welcome c=
ontributions. There are many theorems that can be transcribed from other so=
urces of intuitionistic and relational logic, as well as folk theorems abou=
t Lojban which have not been formalized. There are also theorems which have=
 been transcribed and informally justified but not yet formally proven.<br =
/></div><div><br /></div><div>I also welcome mathboxes [2] from community m=
embers who wish to use my existing work as a starting foundation for their =
own flavors of formal Lojban.<br /></div><div><br /></div><div>mi'e la korv=
o .i di'ai<br /></div><div><br /></div><div>[0] https://mostawesomedude.git=
hub.io/brismu/index.html</div><div>[1] https://mostawesomedude.github.io/br=
ismu/mmtheorems.html</div><div>[2] https://us.metamath.org/ileuni/mathbox.h=
tml</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/f3d0d528-a9bf-43bc-bc02-f4d981c19f7dn%40googlegroups.com?=
utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.com/d/msgid/l=
ojban/f3d0d528-a9bf-43bc-bc02-f4d981c19f7dn%40googlegroups.com</a>.<br />

------=_Part_2651_1317818005.1690913317946--

------=_Part_2650_421532160.1690913317946--