LeanWarp 0.2.3

LeanWarp 0.2.3 is the first PyPI release under the package name leanwarp.

Install with uv tool install leanwarp. Existing GitHub-release users should first run uv tool uninstall leanwarp-sdk; a plain install otherwise conflicts with the existing leanwarp command.

This release includes the qualified feedback workflow, updated agent guidance and SDK update handling. The Python API, CLI and MCP interface are included in one package.

Validation: 421 installed-package tests passed locally. The exported commit passed standalone SDK CI on Python 3.12, 3.13 and 3.14. The compatible production runtime passed its protected migration, deployment and customer journey gates before this export.

Source Cloud commit: d4e2ca93b1147e5b0d3da4e4af3d8458473dd81c
Source SDK tree: a42c778d274b81b4cff852cace5a0cb42d235edd
SDK commit: 26b3325e679deb55f353e812efe13a45d0a1dfdf

LeanWarp SDK 0.2.2

LeanWarp SDK 0.2.2 aligns CLI, MCP and agent guidance with the deployed research runtime and improves account and operation-history handling.

• Hole guidance distinguishes resolved, sorry, unresolved and unknown states. Unknown contexts are reported separately and do not imply proof completion.
• Extraction guidance describes preserved section variables and source-preserving failures.
• Cache the immutable account owner per client, avoiding repeated account reads during project operations.
• Support pagination across larger operation histories and detect repeated cursors.
• Preserve polling through the final fraction of the requested wait budget.

Existing CLI commands, Python entry points and MCP tool names remain compatible. Account limit overrides are operator-controlled; this SDK does not enable them automatically.

Source-Cloud-Commit: 08501532618539b07d021d79db6d8a596854e930
Source-SDK-Tree: 249234a66c89cfa06bcf73f2dbfad95910238d22
Source-SDK-Commit: 4c3df9a73f775f8cbdf9b81ba355e475e43fc2ed

This is an alpha GitHub release; it does not publish a package to PyPI.

SDK CI passed on Python 3.12, 3.13 and 3.14. The attached wheel and source distribution are the exact CI-tested files; SHA256SUMS records their hashes.

Production promotion passed. Independent postflight verified the API, worker and website release identities, all 30 canary checks, exact ledger reconciliation and closure of all four canary allocations.

LeanWarp SDK 0.2.1

LeanWarp SDK 0.2.1 clarifies proof progress and suggestion refusals in the CLI, MCP tools and bundled agent guide.

• holes reports conservative unfinished flags and unfinished_count. A filled ?_ can be marked finished when its known enclosing declaration has no remaining sorry of its own. Literal sorry, anonymous examples and unknown declarations remain flagged. Another sorry in the same proof can keep filled placeholders flagged, so this count is not a count of remaining goals.
• suggest explains refused tactics through rejections. A recheck_incomplete result means verification did not finish; it does not prove the tactic is incorrect.
• Guidance clarifies apply: another successful editing operation replaces its candidate patch; an intervening non-editing operation makes it refuse. wait and status do not replace the candidate.
• sorry2lemma moves an unfinished theorem's proof into a named lemma. The new lemma still needs a proof. Unsupported section variables fail without changing the file.

Existing CLI commands and MCP tool names remain compatible. The new hole and rejection fields require the corresponding hosted runtime update.

Source-Cloud-Commit: 957d4a3dbcbaad06f8c5ad5b613bc3f295ac1271
Source-SDK-Tree: 7af115b840ec48b4af11aca930d3957d49dc7931

The wheel and source distribution attached to this release come from the release commit's successful SDK CI run. SHA256SUMS records their checksums. This is an alpha GitHub release; it does not publish a package to PyPI.

Source-SDK-Commit: 3f80926186ebb145733d4561108b206007b156f4
SDK CI passed on Python 3.12, 3.13 and 3.14. Production promotion passed, with independent API, worker, website and PR130 feature verification before this publication.

LeanWarp SDK 0.1.0 — beta preview

Beta preview of the LeanWarp Python SDK, CLI and local MCP server.

For the current production-compatible SDK, use the repository's main branch:

uv tool install --python 3.12 \
  'leanwarp-sdk @ git+https://github.com/Isagoge-Labs/LeanWarp-SDK.git'

See the getting started guide and agent setup. The SDK is MIT licensed. Hosted execution requires an API key and available account credit.

This tag preserves an earlier SDK snapshot. Its attached wheel and source archive remain unchanged; use the installation command above for the current SDK and documentation.

Original artifact qualification: 63 installed-wheel tests passed on Python 3.12, 3.13 and 3.14, including CLI and local MCP workflows. The attached SHA256SUMS identifies the retained files. These artifacts were built from SDK commit 9c9ef8e0cbf2e5feab3e6ae2c7d243fcbc0209f7.