[lojban-beginners] Re: logical proofs?

[mikevdg@gulik.co.nz]

(a proof that the set of prime numbers has infinitely many members...)

Quoting Robin Lee Powell <rlpowell@digitalkingdom.org>:
> On Mon, Aug 23, 2004 at 03:18:49AM -0400, Andrew Archibald wrote:
> ni'o jarco lo du'u ci'i mulna'usle cei broda cu zasti
> .i sruma lo du'u mi'o ponse lo liste be me'i ci'i broda
> .i ba bo finti ko'a goi lo namcu poi ve jmina li pa lo simxu pilji be ro
> le se liste
> .i ko'a to se nibli lo pu nu jarco toi cu kakne lo nu fendi fi pa
> broda goi ko'e to cumki lo nu du ko'a toi
> .i ku'i ko'e na se fendi fi lo se liste broda .i se ni'i bo su'o broda
> poi na se list cu zasti to cumki lo nu na du ko'a toi
> .i se ni'i bo lo liste be me'i ci'i broda cu na kakne lo nu vasru ro
> broda
> .i fe'o

*phew*. Yea, okay, I'm convinced. Has somebody put a revised version of this on
the wiki? It's all pretty much gibberish to me though.

What I'm interested in is whether it is possible that this could be mechanically
derived, for example by somebody using a proof assistant such as COQ, but using
lojban? I.e are all the steps in the proof mechanical enough to convince a
computer that (e.g.) prime numbers are infinite?

Michael.