From mikevdg@gulik.co.nz Mon Aug 23 14:29:48 2004
Received: with ECARTIS (v1.0.0; list lojban-beginners); Mon, 23 Aug 2004 14:30:29 -0700 (PDT)
Received: from genamics.blastula.net ([205.214.85.184])
	by chain.digitalkingdom.org with esmtp (TLS-1.0:DHE_RSA_3DES_EDE_CBC_SHA:24)
	(Exim 4.34)
	id 1BzMNw-0003Eh-H0
	for lojban-beginners@chain.digitalkingdom.org; Mon, 23 Aug 2004 14:29:48 -0700
Received: from cpanel by genamics.blastula.net with local (Exim 4.34)
	id 1BzMNr-0008Ie-UG
	for lojban-beginners@chain.digitalkingdom.org; Tue, 24 Aug 2004 09:29:43 +1200
Received: from localhost (localhost [127.0.0.1]) 
	by www.gulik.co.nz (IMP) with HTTP 
	for <mikevdg@localhost>; Tue, 24 Aug 2004 09:29:43 +1200
Message-ID: <1093296583.412a61c7e09ce@www.gulik.co.nz>
Date: Tue, 24 Aug 2004 09:29:43 +1200
From: mikevdg@gulik.co.nz
To: lojban-beginners@chain.digitalkingdom.org
Subject: [lojban-beginners] Re: logical proofs?
References: <1093232310.412966b640996@www.gulik.co.nz> <20040823041958.GD3257@chain.digitalkingdom.org> <20040823031849.A32026@fresco.Math.McGill.CA> <20040823153053.GI3257@chain.digitalkingdom.org>
In-Reply-To: <20040823153053.GI3257@chain.digitalkingdom.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
User-Agent: Internet Messaging Program (IMP) 3.2.2
X-Originating-IP: 127.0.0.1
X-MailScanner-Information: Please contact the ISP for more information
X-MailScanner: Found to be clean
X-AntiAbuse: This header was added to track abuse, please include it with any abuse report
X-AntiAbuse: Primary Hostname - genamics.blastula.net
X-AntiAbuse: Original Domain - chain.digitalkingdom.org
X-AntiAbuse: Originator/Caller UID/GID - [32001 32001] / [47 12]
X-AntiAbuse: Sender Address Domain - gulik.co.nz
X-Source: 
X-Source-Args: 
X-Source-Dir: 
X-archive-position: 727
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: mikevdg@gulik.co.nz
Precedence: bulk
Reply-to: lojban-beginners@chain.digitalkingdom.org
X-list: lojban-beginners

(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.