detecting plagiarism

Stream: Lean for teaching

[Thanos Tsouanas]

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]

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

[Arthur Paulino]

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

[Arthur Paulino]

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]

Is this method defeated by a strategically placed id?

[Arthur Paulino]

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]

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]

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]

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