Hacktoberfest 2026: the issues maintainers tagged for October, open and beginner-friendly. Browse Hacktoberfest issues

`leanchecker --from-export` rejects string and quotient rfl proof accepted by `Lean`

Open
  • Is something wrong?
#15,643 1 comment 0 reactions 0 assignees View on GitHub

Maintainers usually reply within 1 day

Nobody has claimed this yet.

Assessment

Difficulty
4/5
Estimated time
3-5 days
Newbie friendliness
48/100
Issue type
Bug
Clarity
Clearly specified
Activity status
Active
Domain
compilers

Research direction

The report names leanchecker --from-export, leanexport, and a minimal Main.lean example. Start by reproducing the failure with the listed nightly commands, then trace how the exported declaration refers to String.ofList and why the checker cannot resolve it. Done means the exported proof passes verification while the reported string and quotient examples remain covered.

Written by the indexing model from the issue text.

Description

bug
Prerequisites
  • Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
  • Reduce the issue to a minimal, self-contained, reproducible test case.
  • Test your test case against the latest nightly release
Description

Lean accepts "a" ++ "b" = "ab" by rfl, but exporting the proof with leanexport and checking it with leanchecker --from-export fails with an unknown-constant error.

Context

The same failure occurs with "ab" = String.mk ['a', 'b']. Using String.ofList explicitly instead of String.mk makes replay succeed.

Steps to Reproduce

  1. Save the following as Main.lean:

    theorem a_append : "a" ++ "b" = "ab" := rfl

  2. With nightly-2026-10-12 installed, run in the same directory:

    TC="$HOME/.elan/toolchains/leanprover--lean4-nightly---nightly-2026-10-12/bin"
export LEAN_SYSROOT="$TC/.." LEAN_PATH=".:$TC/../lib/lean"
"$TC/lean" -o Main.olean Main.lean
"$TC/leanexport" Main -- a_append > Main.ndjson
"$TC/leanchecker" --from-export Main.ndjson

Expected behavior: The exported proof passes verification.

Actual behavior: Compilation and export succeed. #print axioms reports [propext]. Replay exits with code 1:

Lean default kernel rejects the solution: while replaying declaration 'a_append':
(kernel) unknown constant 'String.ofList'
Versions
version 4.36.0-nightly-2026-10-12
Additional Information

NA

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Dominant language
Lean
Stars
9.6k
Forks
1.1k
Avg merge
1d 2h
Merged PRs (30d)
301

Getting set up

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from leanprover/lean4

All issues in leanprover/lean4

Similar issues

More Compilers issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.