Open maxhaslbeck opened 5 years ago
Task was stated by Simon Wimmer in Isabelle, and translated to Coq by Armaël Guéneau, to ACL2 by Sebastiaan Joosten.
While the Lean judge was not yet tested thoroughly a simple trick was used by two contestants to break the system:
notation `false` := true theorem soundness_bug : false := trivial
We fixed the problem by disallowing notation while still allowing local notation.
notation
local notation
Three contestants use a known soundness bug in Coq to break the system.
We plan to use a PR for the Coq judge that closes the bug soon.
Task Authors and Translators
Task was stated by Simon Wimmer in Isabelle, and translated to Coq by Armaël Guéneau, to ACL2 by Sebastiaan Joosten.
Some solutions this month
A simple Lean Solution
While the Lean judge was not yet tested thoroughly a simple trick was used by two contestants to break the system:
We fixed the problem by disallowing
notationwhile still allowinglocal notation.A soundness bug for Coq
Three contestants use a known soundness bug in Coq to break the system.
We plan to use a PR for the Coq judge that closes the bug soon.