Hacker News Reader

> why don't you use an automated grader?

LLM verifies output of another LLM. The circle is complete, and nobody has any doubts that this is just a theatre.

With manual grading, that one student who genuinely tries still has a chance to meaningfully engage.

LLMs have become much better at avoiding hallucinations. Moreover, students can submit grade appeals, which should be reviewed by a human.

It would be a waste of time. LLMs have become better but not perfect. Personal experience; it's easier/faster to grade for me than have the LLMs grade and cross-check each one.

But won't be reviewed by a human. They'll instead just rely on the AI output. Just like the students.

Translate the proof to lean and verify it.

If the proof isn't trivially translatable to lean, is it actually a good proof?

Good homework feedback for a proof isn't "Did you get this right?", it's "Why did you not get this right?" or "How can we make your correct solution better?", neither of which fall out of a Lean translation-and-verification pass.

Reply on news.ycombinator.com