[lojban-beginners] Re: logical proofs?

[Robin Lee Powell <rlpowell@digitalkingdom.org>]

On Tue, Aug 24, 2004 at 09:29:43AM +1200, mikevdg@gulik.co.nz wrote:
> (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? 

No, but I suppose somebody could.  :-)

That's your cue.

> It's all pretty much gibberish to me though.

Not surprised.

> 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?

Rob Speer is working on something like this.  Rob?

-Robin

-- 
http://www.digitalkingdom.org/~rlpowell/ *** http://www.lojban.org/
Reason #237 To Learn Lojban: "Homonyms: Their Grate!"