[TYPES] AI-generated conference submissions

[Gavin Mendel-Gleason]

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.

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