Issues

• Option to skip the builtin kernel replay when an external kernel is used

  leanprover/comparator#97 · Filter by author mt0-svg opened on Oct 1, 2026

• Optional parallel kernel replay

  leanprover/comparator#95 · Filter by author dpwoodru opened on Oct 1, 2026

• Lean kernel replay rejects any theorem whose proof reduces a string literal

  leanprover/comparator#93 · Filter by author ASamSam opened on Sep 21, 2026

• Comparator calls landrun with --best-effort

  leanprover/comparator#83 · Filter by author tadamcz opened on Aug 24, 2026
  5

• [Feature Request] Mutli-file challenge support

  leanprover/comparator#79 · Filter by author rusch95 opened on Aug 20, 2026
  1

• Untrusted descendants can outlive safeLakeBuild

  leanprover/comparator#77 · Filter by author kim-em opened on Aug 20, 2026
  2

• Proof irrelevance is not respected in statements

  leanprover/comparator#59 · Filter by author eric-wieser opened on Jul 17, 2026
  1

• Comparator generates different instance names for problem and solution files

  leanprover/comparator#58 · Filter by author eric-wieser opened on Jul 17, 2026
  7

• Incorrectly adding propext with nanoda kernel

  leanprover/comparator#51 · Filter by author stephen-huan opened on Jun 6, 2026
  1

• Better errors when the lean4export version is incorrect

  enhancement
  leanprover/comparator#33 · Filter by author robsimmons opened on Apr 20, 2026

• Display both types in "Challenge and solution theorem statement do not match"

  leanprover/comparator#9 · Filter by author JasonGross opened on Dec 22, 2025

• comparator should permit dependent challenges ("Const does not match" is sometimes a lie)

  leanprover/comparator#4 · Filter by author JasonGross opened on Dec 20, 2025
  1

• "uncaught exception: Challenge and solution constant kind don't match" is both unhelpful and untrue

  leanprover/comparator#3 · Filter by author JasonGross opened on Dec 19, 2025
  6