From rlpowell@digitalkingdom.org Mon Aug 23 14:47:59 2004
Received: with ECARTIS (v1.0.0; list lojban-beginners); Mon, 23 Aug 2004 14:47:59 -0700 (PDT)
Received: from rlpowell by chain.digitalkingdom.org with local (Exim 4.34)
	id 1BzMfX-0003Xb-Hm
	for lojban-beginners@chain.digitalkingdom.org; Mon, 23 Aug 2004 14:47:59 -0700
Date: Mon, 23 Aug 2004 14:47:59 -0700
To: lojban-beginners@chain.digitalkingdom.org
Subject: [lojban-beginners] Re: logical proofs?
Message-ID: <20040823214759.GE3257@chain.digitalkingdom.org>
References: <1093232310.412966b640996@www.gulik.co.nz> <20040823041958.GD3257@chain.digitalkingdom.org> <20040823031849.A32026@fresco.Math.McGill.CA> <20040823153053.GI3257@chain.digitalkingdom.org> <1093296583.412a61c7e09ce@www.gulik.co.nz>
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <1093296583.412a61c7e09ce@www.gulik.co.nz>
User-Agent: Mutt/1.5.6+20040722i
From: Robin Lee Powell <rlpowell@digitalkingdom.org>
X-archive-position: 729
X-Approved-By: rlpowell@digitalkingdom.org
X-ecartis-version: Ecartis v1.0.0
Sender: lojban-beginners-bounce@chain.digitalkingdom.org
Errors-to: lojban-beginners-bounce@chain.digitalkingdom.org
X-original-sender: rlpowell@digitalkingdom.org
Precedence: bulk
Reply-to: lojban-beginners@chain.digitalkingdom.org
X-list: lojban-beginners

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!"