Skip to content

Simple Query

This guide will walk you through performing a simple proof verification using both synchronous and asynchronous clients.

Synchronous Client

The synchronous client is straightforward to use and is suitable for most common use cases.

API Reference: verify

The client.verify() method sends a proof to the server and synchronously waits for the verification result.

Function Signature

def verify(
    self,
    proof: str | Path | os.PathLike,
    config: ProofConfig | None = None
) -> ProofResult:

Parameters

  • proof (str | Path | os.PathLike): The proof to be verified. This can be provided in several ways:

    • A string containing the Lean code.
    • A pathlib.Path object pointing to a .lean file.
    • A string representing the path to a .lean file.

  • config (ProofConfig | None, optional): A configuration object to customize the verification process. If not provided, default settings are used. See the Proof Configuration page for details on available options.

Returns

  • ProofResult: A Pydantic model containing the verification results, including status, and any potential errors.

Example

Verifying a proof

Here's how to verify a simple proof using the LeanClient:

from lean_runner import LeanClient

# Initialize the client with the server's base URL
client = LeanClient("http://localhost:8000")

# Define the proof as a string
proof_content = (
    "import Mathlib.Tactic.NormNum\n"
    "theorem test : 2 + 2 = 4 := by norm_num"
)

# Verify the proof
result = client.verify(proof_content)

# Print the result
print(result.model_dump_json(indent=4))

# The client should be closed when no longer needed
client.close()

{
    "success": true,
    "status": "finished",
    "result": {
        "env": 0,
        "messages": []
    },
    "error_message": null
}

Using a with statement

You can use a with statement to manage the client's lifecycle automatically:

from lean_runner import LeanClient

with LeanClient("http://localhost:8000") as client:
    proof_content = (
        "import Mathlib.Tactic.NormNum\n"
        "theorem test : 2 + 2 = 4 := by norm_num"
    )
    result = client.verify(proof_content)
    print(result.model_dump_json(indent=4))

{
    "success": true,
    "status": "finished",
    "result": {
        "env": 0,
        "messages": []
    },
    "error_message": null
}

Asynchronous Client

The asynchronous client is ideal for applications that require high concurrency and non-blocking I/O.

API Reference: verify

The client.verify() method sends a proof to the server and asynchronously awaits the verification result.

Function Signature

async def verify(
    self,
    proof: str | Path | os.PathLike | AnyioPath,
    config: ProofConfig | None = None,
) -> ProofResult:

Parameters

  • proof (str | Path | os.PathLike | AnyioPath): The proof to be verified. This can be provided as:

    • A string containing the Lean code.
    • A pathlib.Path or anyio.Path object pointing to a .lean file.
    • A string representing the path to a .lean file.

  • config (ProofConfig | None, optional): A configuration object to customize the verification process. If not provided, default settings are used. See the Proof Configuration page for details on available options.

Returns

  • ProofResult: A Pydantic model containing the verification results.

Example

Verifying a proof asynchronously

Here's the same example using the AsyncLeanClient:

import asyncio
from lean_runner import AsyncLeanClient

async def main():
    # Initialize the async client
    async with AsyncLeanClient("http://localhost:8000") as client:
        proof_content = (
            "import Mathlib.Tactic.NormNum\n"
            "theorem test : 2 + 2 = 4 := by norm_num"
        )
        result = await client.verify(proof_content)
        print(result.model_dump_json(indent=4))

if __name__ == "__main__":
    asyncio.run(main())

{
    "success": true,
    "status": "finished",
    "result": {
        "env": 0,
        "messages": []
    },
    "error_message": null
}

In this example, async with ensures the client session is properly closed. The await client.verify() call performs the verification without blocking the event loop.