Path: csiph.com!eternal-september.org!feeder.eternal-september.org!nntp.eternal-september.org!.POSTED!not-for-mail
From: Ben Bacarisse <ben@bsb.me.uk>
Newsgroups: comp.theory
Subject: Re: is the ct-thesis cooked?
Date: Tue, 20 Jan 2026 00:50:46 +0000
Organization: A noiseless patient Spider
Lines: 19
Message-ID: <87ldhtt8d5.fsf@bsb.me.uk>
References: <10hct1p$1d92l$1@solani.org> <dbe9c3aa-42f9-496d-9394-a2d3205f9138@gmail.com> <10jiem1$3j7nf$1@dont-email.me> <10jkcoo$9u4l$1@dont-email.me> <10jkiea$b3m5$4@dont-email.me> <yt59R.1403595$u2q8.729303@fx11.iad> <10k3re3$2krfs$1@dont-email.me> <AOi9R.203777$Zqk9.36159@fx08.iad> <10k4h87$2s63u$1@dont-email.me> <cCq9R.1474415$u2q8.939156@fx11.iad> <10k6a6e$3aum9$4@dont-email.me> <LnZ9R.47138$KF5d.24431@fx43.iad> <10kam87$ofu9$1@dont-email.me> <4fiaR.134641$Ij5a.121807@fx15.iad> <10kcv63$18ne5$1@dont-email.me> <4YtaR.289653$ZkQ4.281544@fx47.iad> <10kedkg$21adq$1@dont-email.me> <87wm1ht4d5.fsf@bsb.me.uk> <10kglpr$2nl2r$2@dont-email.me> <87qzrntz2h.fsf@bsb.me.uk> <10kif7l$3bqdj$3@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain
Injection-Date: Tue, 20 Jan 2026 00:50:48 +0000 (UTC)
Injection-Info: dont-email.me; posting-host="97816dd9aadb437b2cb5e4f61b5cafec"; logging-data="871804"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX18mBDJdQe2X1aOkaur2IC7Fy90pHQZPjX4="
User-Agent: Gnus/5.13 (Gnus v5.13)
Cancel-Lock: sha1:l4BBaVmAPfW8Rq51olFvTkf749M= sha1:i1Dp5TeWD2OLYdJPXjYN8po3Wkw=
X-BSB-Auth: 1.5796b6cbdad4a71a83d2.20260120005046GMT.87ldhtt8d5.fsf@bsb.me.uk
Xref: csiph.com comp.theory:139263

Tristan Wibberley <tristan.wibberley+netnews2@alumni.manchester.ac.uk>
writes:

> On 18/01/2026 02:49, Ben Bacarisse wrote:
>> Ideas are, sadly, easily come by.  Well-defined models and proofs are
>> rather harder.  Good luck.
>
> Is that nothing more than the difference between constraints and
> constructions?

No.

> That can be helped by automated theorem provers, do you know the current
> state of the art?

Yes.

-- 
Ben.