Search results

"PANIC at Canonical.fromTerm" when trying to prove a simple theorem about RCLike elements

Status: Open.

#31 In chasenorman/CanonicalLean;

· SageBinder opened on Oct 1, 2025

Proof not found for equivalence test on Artin_exercise_13_4_10

performanceDifficult user-submitted instancesDifficult user-submitted instances

Status: Open.

#29 In chasenorman/CanonicalLean;

· egfiwhfe opened on Sep 12, 2025

Canonical is able to prove around 14% of bidirectional equivalence in the ProofVerif dataset

Status: Open.

#28 In chasenorman/CanonicalLean;

· egfiwhfe opened on Sep 12, 2025

Canonical crashes when searching for proof

Status: Open.

#27 In chasenorman/CanonicalLean;

· egfiwhfe opened on Sep 11, 2025

Canonical proof rejected by Lean

Status: Open.

#26 In chasenorman/CanonicalLean;

· egfiwhfe opened on Sep 10, 2025

Canonical failed to build on Apple Silicon

Status: Open.

#17 In chasenorman/CanonicalLean;

· BoltonBailey opened on May 31, 2025

Too modest relative performance numbers given in Canonical.mp4

Status: Open.

#11 In chasenorman/CanonicalLean;

· euprunin opened on May 5, 2025

Immediate No proof found despite high timeout

Status: Open.

#5 In chasenorman/CanonicalLean;

· Vilin97 opened on Apr 18, 2025