Metrics API Reference

The Metrics module provides a suite of tools for evaluating formal mathematics. These classes allow you to assess the syntactic correctness, equivalence, and quality of Lean 4 code, ranging from simple typechecking to semantic comparisons using LLMs.

Base Metric

MetricBatchMetric

`leanflow.Metric`

Bases: ABC

Abstract base class for stateless metrics.

The compute method is synchronous, making it compatible with multiprocessing.

`name` `property`

Returns the snake_case name of the metric class.

Returns:

Type	Description
`str`	The name of the metric.

`init(metric_config={}, repl_config={}, client=None, **shared_dependencies)`

Initializes the metric.

Parameters:

Name	Type	Description	Default
`metric_config`	`dict[str, Any]`	Configuration dictionary for the metric.	`{}`
`repl_config`	`dict[str, Any]`	Configuration for REPL/Client (e.g. {'lean_version': ...}).	`{}`
`client`	`Optional[Client]`	Existing client instance to share.	`None`
`**shared_dependencies`	`Any`	Other shared dependencies.	`{}`

`compute(*args, **kwargs)`

Synchronously computes the metric for a single example.

This method is the entrypoint for a multiprocessing worker. It calls the REPL asynchronously and returns the result.

Parameters:

Name	Type	Description	Default
`*args`	`Any`	Positional arguments for the metric check.	`()`
`**kwargs`	`Any`	Keyword arguments for the metric check.	`{}`

Returns:

Type	Description
`Any`	The result of the metric computation.

`get_runner()`

Returns the appropriate LeanRunner and context manager.

Returns:

Type	Description
`tuple[runner, context]`	The runner and an appropriate context manager. - For reusable clients: (client, NoOpAsyncContextManager()) - For fresh instances: (instance, instance)

`run_check_async(*args, **kwargs)` `abstractmethod` `async`

Asynchronously computes the metric for a single example.

Parameters:

Name	Type	Description	Default
`*args`	`Any`	Positional arguments for the metric check.	`()`
`**kwargs`	`Any`	Keyword arguments for the metric check.	`{}`

Returns:

Type	Description
`Any`	The result of the metric computation.

`leanflow.BatchMetric`

Bases: Metric

Base class for metrics that can be computed on a batch of examples.

`compute_batch(examples)`

Synchronously computes the metric for a batch of examples.

Parameters:

Name	Type	Description	Default
`examples`	`list[Any]`	A list of examples to process.	required

Returns:

Type	Description
`Any`	The result of the batch computation.

Raises:

Type	Description
`LeanValueError`	If `examples` is not a list.

`run_batch_async(examples)` `abstractmethod` `async`

Asynchronously computes the metric for a batch of examples.

Parameters:

Name	Type	Description	Default
`examples`	`list[Any]`	List of examples to process.	required

Returns:

Type	Description
`Any`	The result of the metric computation.

Interactive Metrics

These metrics run on individual examples and typically rely on the Lean REPL to verify logic or proofs.

TypeCheckBEqPlusBEqLEquivRfl

`leanflow.TypeCheck`

Bases: Metric

Runs a Lean statement through the REPL and checks for errors during compilation. Returns True when there are no errors returned from Lean.

Example

from leanflow import TypeCheck

metric = TypeCheck(repl_config={"lean_version": "4.24.0"})
result = metric.compute("theorem test : 1 + 1 = 2 := rfl")
print(result)

`init(metric_config={}, repl_config={}, client=None, **shared_dependencies)`

Initializes the TypeCheck metric.

Parameters:

Name	Type	Description	Default
`metric_config`	`dict[str, Any]`	Configuration dictionary.	`{}`
`repl_config`	`dict[str, Any]`	Configuration for the REPL (e.g. {'lean_version': '4.21.0'}).	`{}`
`client`	`Optional[Client]`	An existing Client instance to use.	`None`
`**shared_dependencies`	`Any`	Other shared dependencies.	`{}`

`run_check_async(statement, header=None)` `async`

Typechecks a Lean statement.

Parameters:

Name	Type	Description	Default
`statement`	`str`	The Lean code to typecheck.	required
`header`	`Optional[str]`	Optional header (imports, etc.) to prepend.	`None`

Returns:

Type	Description
`bool`	True if the statement typechecks without errors, False otherwise.

`leanflow.BEqPlus`

Bases: Metric

Computes the BEq+ metric by checking for bidirectional provability using a variety of tactics. Source: Reliable Evaluation and Benchmarks for Statement Autoformalization (Poiroux et al., EMNLP 2025).

Example

from leanflow import BEqPlus

thm1 = "theorem t1 (a b c : Prop) : a ∧ b → c := by sorry"
thm2 = "theorem t2 (a b c : Prop) : a → b → c := by sorry"

metric = BEqPlus(repl_config={"lean_version": "4.24.0"})
result = metric.compute(thm1, thm2, header="import Mathlib")
print(result)

`init(metric_config={}, **shared_dependencies)`

Initializes the BEqPlus metric.

Parameters:

Name	Type	Description	Default
`metric_config`	`dict[str, Any]`	Configuration dictionary.	`{}`
`**shared_dependencies`	`Any`	Shared dependencies. Must include 'repl_config' or 'client'.	`{}`

`run_check_async(statement_1, statement_2, header=None)` `async`

Computes the BEq+ equivalence for the given example.

Parameters:

Name	Type	Description	Default
`statement_1`	`str`	The first Lean statement.	required
`statement_2`	`str`	The second Lean statement.	required
`header`	`Optional[str]`	Optional header (imports, etc.) to prepend.	`None`

Returns:

Type	Description
`bool`	True if both statements can prove each other, False otherwise.

`leanflow.BEqL`

Bases: Metric

Computes the BEq-L metric by checking for bidirectional equivalence using exact?. Source: Reliable Evaluation and Benchmarks for Statement Autoformalization (Poiroux et al., EMNLP 2025)

Example

from leanflow import BEqL

thm1 = "theorem t1 (a b c : Prop) : a ∧ b → c := by sorry"
thm2 = "theorem t2 (a b c : Prop) : a → b → c := by sorry"

metric = BEqL(repl_config={"lean_version": "4.24.0"})
result = metric.compute(thm1, thm2)
print(result)

`init(metric_config={}, **shared_dependencies)`

Initializes the BEqL metric.

Parameters:

Name	Type	Description	Default
`metric_config`	`dict[str, Any]`	Configuration dictionary.	`{}`
`**shared_dependencies`	`Any`	Shared dependencies. Must include 'repl_config' or 'client'.	`{}`

`run_check_async(statement_1, statement_2, header=None)` `async`

Checks if statement_1 and statement_2 are equivalent using exact?.

Parameters:

Name	Type	Description	Default
`statement_1`	`str`	The first Lean statement.	required
`statement_2`	`str`	The second Lean statement.	required
`header`	`Optional[str]`	Optional header (imports, etc.) to prepend.	`None`

Returns:

Type	Description
`bool`	True if both statements can prove each other using `exact?`, False otherwise.

`leanflow.EquivRfl`

Bases: Metric

Computes equivalence by checking for definitional equality using rfl. Source: Conjecturing: An Overlooked Step in Formal Mathematical Reasoning (Sivakumar et al., ArXiv 2025)

Example

from leanflow import EquivRfl

conjecture_1 = "abbrev foo : Nat := 2"
conjecture_2 = "abbrev bar : Nat := 1 + 1"

metric = EquivRfl(repl_config={"lean_version": "4.24.0"})
result = metric.compute(conjecture_1, conjecture_2)
print(result)

`init(metric_config={}, **shared_dependencies)`

Initializes the EquivRfl metric.

Parameters:

Name	Type	Description	Default
`metric_config`	`dict[str, Any]`	Configuration dictionary.	`{}`
`**shared_dependencies`	`Any`	Shared dependencies. Must include 'repl_config' or 'client'.	`{}`

`run_check_async(statement_1, statement_2, header=None)` `async`

Checks for definitional equality between two statements.

Parameters:

Name	Type	Description	Default
`statement_1`	`str`	The first Lean statement.	required
`statement_2`	`str`	The second Lean statement.	required
`header`	`Optional[str]`	Optional header (imports, etc.) to prepend.	`None`

Returns:

Type	Description
`bool`	True if the statements are definitionally equal, False otherwise.

LLM & Batch Metrics

These metrics leverage LLMs to perform semantic evaluations. They are designed to process inputs in batches.

LLMGraderBEqConJudge

`leanflow.LLMGrader`

Bases: LLMAsAJudge

Computes semantic equivalence using a LLM-as-a-judge. Source: FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models (Yu et al., ArXiv 2025).

This metric performs back-translation of formal statements to natural language using the backtranslation model and then uses the comparison model to compare the semantic equivalence of the back-translated statements.

Example

from leanflow import LLMGrader

data = {
    "formal_statement": "theorem t1 (a b c : Prop) : a ∧ b → c := by sorry",
    "formal_statement_generated": "theorem t2 (a b c : Prop) : a → b → c := by sorry"
}

metric = LLMGrader(
    api_config={"base_url": "<URL>", "api_key": "<KEY>"},
    backtranslation={"model": "deepseek-math"},
    comparison={"model": "gpt-4"},
)

result = metric.compute_batch([data])
print(result)

`init(metric_config={}, **shared_dependencies)`

Initializes the LLMGrader metric.

Parameters:

Name	Type	Description	Default
`metric_config`	`dict[str, Any]`	Configuration dictionary.	`{}`
`**shared_dependencies`	`Any`	Shared dependencies.	`{}`

Raises:

Type	Description
`LeanEnvironmentError`	If `use_vllm` is True but vLLM is not installed.

`run_batch_async(examples)` `async`

Computes the LLM grader metric for a batch of examples.

Parameters:

Name	Type	Description	Default
`examples`	`list[dict[str, Any]]`	List of examples to process.	required

Returns:

Type	Description
`list[dict[str, Any]]`	List of results, each containing 'llm_grader' (bool) and raw outputs.

`leanflow.BEq`

Bases: BatchMetric

Computes the BEq metric using a heuristic check followed by LLM-based tactic generation. Source: Rethinking and Improving Autoformalization: Towards a Faithful Metric and a Dependency Retrieval-based Approach (Liu et al., 2024)

First tries a heuristic exact? check. If that fails, it uses an LLM in a loop to generate and validate tactics to prove equivalence.

Example

from leanflow import BEq

data = {
    "header": "import Mathlib"
    "formal_statement": "theorem t1 (a b c : Prop) : a ∧ b → c := by sorry",
    "formal_statement_generated": "theorem t2 (a b c : Prop) : a → b → c := by sorry",
}

metric = BEq(
    api_config={"base_url": "<URL>", "api_key": "<KEY>"},
    tactic_generator={"model": "deepseek-math"},
    repl_config={"lean_version": "v4.24.0"}
)

result = metric.compute_batch([data])
print(result)

`init(metric_config={}, **shared_dependencies)`

Initializes the BEq metric.

Parameters:

Name	Type	Description	Default
`metric_config`	`dict[str, Any]`	Configuration dictionary.	`{}`
`**shared_dependencies`	`Any`	Shared dependencies. Must include 'repl_config' or 'client'.	`{}`

Raises:

Type	Description
`LeanValueError`	If neither 'repl_config' nor 'client' is provided, or if 'tactic_generator.model' is missing.

`run_batch_async(examples)` `async`

Computes the BEq metric for a batch of examples.

Parameters:

Name	Type	Description	Default
`examples`	`list[dict[str, Any]]`	List of examples to process.	required

Returns:

Type	Description
`list[dict[str, Any]]`	List of results, each containing 'beq' (bool) and 'generated_tactics'.

`leanflow.ConJudge`

Bases: LLMAsAJudge

Judges if a generated Lean statement correctly incorporates a given conjecture using an LLM. Source: Conjecturing: An Overlooked Step in Formal Mathematical Reasoning (Sivakumar et al., ArXiv 2025)

Example

from leanflow import ConJudge

data = {
    "header": "import Mathlib",
    "formal_conjecture": "abbrev conjecture : ℕ : 13",
    "formal_statement": "theorem hackmath_4 : IsLeast {n | ∀ f : Fin n → Fin 12, ∃ a b, f a = f b} ((conjecture) : ℕ ) := by sorry",
    "formal_statement_generated": "theorem hackmath_4 : IsLeast {n | ∀ f : Fin n → Fin 12, ∃ a b, f a = f b} (26 / 2 : ℕ ) := by sorry",
}

metric = ConJudge(
    api_config={"base_url": "<URL>", "api_key": "<KEY>"},
    comparison={"model": "gpt-4"}
)

result = metric.compute_batch([data])
print(result)

`init(metric_config={}, **shared_dependencies)`

Initializes the ConJudge metric.

Parameters:

Name	Type	Description	Default
`metric_config`	`dict[str, Any]`	Configuration dictionary.	`{}`
`**shared_dependencies`	`Any`	Shared dependencies.	`{}`

Raises:

Type	Description
`LeanEnvironmentError`	If `use_vllm` is True but vLLM is not installed.

`run_batch_async(examples)` `async`

Computes the ConJudge metric for a batch of examples.

Parameters:

Name	Type	Description	Default
`examples`	`list[dict[str, Any]]`	List of examples to process.	required

Returns:

Type	Description
`list[dict[str, Any]]`	List of results, each containing 'conjudge' (bool) and raw outputs.

Metrics API Reference

Base Metric

leanflow.Metric

name property

__init__(metric_config={}, repl_config={}, client=None, **shared_dependencies)

compute(*args, **kwargs)

get_runner()

run_check_async(*args, **kwargs) abstractmethod async

leanflow.BatchMetric

compute_batch(examples)

run_batch_async(examples) abstractmethod async

Interactive Metrics

leanflow.TypeCheck

__init__(metric_config={}, repl_config={}, client=None, **shared_dependencies)

run_check_async(statement, header=None) async

leanflow.BEqPlus

__init__(metric_config={}, **shared_dependencies)

run_check_async(statement_1, statement_2, header=None) async

leanflow.BEqL

__init__(metric_config={}, **shared_dependencies)

run_check_async(statement_1, statement_2, header=None) async

leanflow.EquivRfl

__init__(metric_config={}, **shared_dependencies)

run_check_async(statement_1, statement_2, header=None) async

LLM & Batch Metrics

leanflow.LLMGrader

__init__(metric_config={}, **shared_dependencies)

run_batch_async(examples) async

leanflow.BEq

__init__(metric_config={}, **shared_dependencies)

run_batch_async(examples) async

leanflow.ConJudge

__init__(metric_config={}, **shared_dependencies)

run_batch_async(examples) async

`leanflow.Metric`

`name` `property`

`init(metric_config={}, repl_config={}, client=None, **shared_dependencies)`

`compute(*args, **kwargs)`

`get_runner()`

`run_check_async(*args, **kwargs)` `abstractmethod` `async`

`leanflow.BatchMetric`

`compute_batch(examples)`

`run_batch_async(examples)` `abstractmethod` `async`

`leanflow.TypeCheck`

`init(metric_config={}, repl_config={}, client=None, **shared_dependencies)`

`run_check_async(statement, header=None)` `async`

`leanflow.BEqPlus`

`init(metric_config={}, **shared_dependencies)`

`run_check_async(statement_1, statement_2, header=None)` `async`

`leanflow.BEqL`

`init(metric_config={}, **shared_dependencies)`

`run_check_async(statement_1, statement_2, header=None)` `async`

`leanflow.EquivRfl`

`init(metric_config={}, **shared_dependencies)`

`run_check_async(statement_1, statement_2, header=None)` `async`

`leanflow.LLMGrader`

`init(metric_config={}, **shared_dependencies)`

`run_batch_async(examples)` `async`

`leanflow.BEq`

`init(metric_config={}, **shared_dependencies)`

`run_batch_async(examples)` `async`

`leanflow.ConJudge`

`init(metric_config={}, **shared_dependencies)`

`run_batch_async(examples)` `async`