Build a Representer for the Lean track

Programming Lean
1

Hi,

I’d like to propose building a representer for the Lean track.

Currently, the Lean track has no representer, which means mentors need to review every solution individually even when they are structurally identical. A representer would normalize
student solutions so that functionally equivalent submissions are grouped together, making mentoring more scalable.

The representer would handle common Lean-specific normalizations such as:

  • Renaming user-defined variables and functions to placeholders
  • Normalizing whitespace and formatting
  • Removing comments and docstrings
  • Standardizing namespace/open declarations

This would allow mentors to write a single piece of feedback that applies to all structurally similar solutions.

Related issue: issues/155

I’d be happy to work on the implementation.

Thanks!

2

How would it work? You have described the goals of a representer, but not how a Lean representer might be implemented.

3

How a Lean representer would work

Interface (required by Exercism)

The representer receives three arguments: exercise slug, solution directory, output directory. It must produce:

  • representation.txt — normalized source code with placeholders
  • mapping.json — maps placeholders back to original names (e.g. {“PLACEHOLDER_1”: “myHelper”})
  • representation.json — metadata with a version field

Implementation approach: Lean 4’s own parser

The key insight is that Lean 4 exposes its parser as a library. Rather than writing fragile regex-based transformations, the representer would:

  1. Parse the student’s .lean file using Lean.Parser to get a Lean.Syntax tree
  2. Walk the syntax tree to apply normalizations
  3. Pretty-print the normalized tree back to source

This is the same approach used by the Elixir representer (Elixir’s Code.string_to_quoted) and the Python representer (ast.parse). Using the language’s own parser is the standard, most
robust strategy.

Example transformation

Input (HelloWorld.lean):
– My first exercise!
namespace HelloWorld
def hello : String :=
let greeting := "Hello, "
let target := “World!”
greeting ++ target
end HelloWorld

representation.txt:
namespace HelloWorld
def hello : String :=
let PLACEHOLDER_1 := "Hello, "
let PLACEHOLDER_2 := “World!”
PLACEHOLDER_1 ++ PLACEHOLDER_2
end HelloWorld

mapping.json:
{
“PLACEHOLDER_1”: “greeting”,
“PLACEHOLDER_2”: “target”
}