Zulip Chat Archive

Stream: Lean for teaching

Topic: detecting plagiarism

Thanos Tsouanas (Nov 01 2022 at 05:59):

Anyone has had success with detecting plagiarism in Lean assignments?
I was thinking that a great aid would be to have Lean output the proof terms constructed by the students using tactic mode, in a way that the output would ignore a student's choice of names. Any idea how I can get Lean to output this? (The objective is to detect solutions that are identical up to α-renaming.)

Sarah Smith (Nov 10 2022 at 20:41):

This is a really interesting question, I also am curious if and how anyone has managed this before^

Arthur Paulino (Dec 11 2022 at 11:48):

Name-irrelevant content addressing can solve this problem. We are tackling it here: https://github.com/yatima-inc/yatima-lang/wiki

Arthur Paulino (Dec 11 2022 at 11:50):

In fact, that part of the stack is already solved. To detect plagiarism between two proofs, one could compare the anon hashes of the respective proof terms.

Jannis Limperg (Dec 11 2022 at 12:18):

Is this method defeated by a strategically placed id?

Arthur Paulino (Dec 11 2022 at 12:23):

Yes, exact matches between hashes might be too rigid. Maybe a fuzzy match between the respective anon IPLD nodes that we create might work better

Martin Dvořák (Dec 12 2022 at 13:41):

Jannis Limperg said:

Is this method defeated by a strategically placed id?

All methods are defeated if the students know what methods you use. That said, some methods are more robust than others (detecting more plagiarism when the students don't know about it).

Shreyas Srinivas (Feb 07 2023 at 18:29):

Question: How do you identify plagiarism if there are maybe not more than one or two straightforward ways to do a proof? There may be other, more terse and neat ways of proving stuff, but at least my first instinct is usually to find the obvious proof, and use typical identifier names (for example n is my induction variable for any induction involving Naturals).

Martin Dvořák (Feb 24 2023 at 23:35):

You cannot identify plagiarism in very easy assignments. I don't think it is a Lean problem tho.

Last updated: Dec 20 2023 at 11:08 UTC