[TYPES] AI-generated conference submissions

[Hendrik Boom]

On Fri, Mar 20, 2026 at 09:38:53AM +0100, Gavin Mendel-Gleason wrote:
> I'm frankly amazed that anyone can hold such a position at the present
> moment.
> 
> I would strongly recommend using an LLM to perform proof search. This is
> not an eliza. They are effective at devising lemmata and can radically
> increase the rate of development.

That is very different from trusting the LLM output.

LLMs are very good at producing plausible-looking output with subtle flaws.
This produces the appearance of progress.  I would not trust an
LLM-generated proof unless it has been vetted by a formal proof-checker
like coq or Lean.

-- hendrik

> 
> Gavin
> 
> On Wed, 18 Mar 2026 at 22:22, Hendrik Boom <hendrik at topoi.pooq.com> wrote:
> 
> > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list 
> > ]
> >
> > On Tue, Mar 17, 2026 at 05:46:39PM -0700, Michael Shulman wrote:
> > > [ The Types Forum,
> > http://lists.seas.upenn.edu/mailman/listinfo/types-list   ]
> > >
> > > I think in Jon's phrase "something that you knowingly haven't
> > understood",
> > > the word "you" refers to all the authors of the paper.  They may not
> > > individually understand all parts of the paper, but as long as at least
> > one
> > > of them understands each part, they can assert that collectively they
> > > understand it.  An AI is qualitatively different because it cannot take
> > > responsibility, hence cannot be a co-author.
> > >
> > > It may be easy for students to fall into the trap of thinking that the AI
> > > "understands" what it told them and therefore they don't have to.  That
> > > doesn't make it okay; it means they need to be educated, gently and
> > firmly.
> >
> > Ever since the Eliza program, AIs have been designed to project the
> > illusion of understanding.  There have been decades of development
> > to this end.  It's not surprising that students fall for it.
x> >
> > -- hendrik
> >