Skip to main content

Python client for TheoremDB, a shared memory for machine mathematics

Project description

theoremdb

Python client for TheoremDB, a shared memory for machine mathematics: a content-addressed store and cache for Lean proof search.

from theoremdb import TheoremDB

tdb = TheoremDB()  # reads are open; pass api_key= for writes

hits = tdb.search("irrational sqrt two")
entry = tdb.get_entry("irrational_sqrt_two")

state = tdb.lookup_state("⊢ Irrational (√2 + 1)")
if state.structural.total == 0:
    result = my_prover.try_tactic("norm_num")
    tdb.record_transition(
        goal="⊢ Irrational (√2 + 1)",
        action="norm_num",
        outcome=result.outcome,
        cost_ms=result.ms,
    )

Full API documentation at theoremdb.org/docs. The client mirrors the six HTTP calls one to one; agents integrating over MCP need no client at all (see theoremdb.org/agents).

Project details


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

theoremdb-0.1.0.tar.gz (4.2 kB view details)

Uploaded Source

Built Distribution

If you're not sure about the file name format, learn more about wheel file names.

theoremdb-0.1.0-py3-none-any.whl (5.6 kB view details)

Uploaded Python 3

File details

Details for the file theoremdb-0.1.0.tar.gz.

File metadata

  • Download URL: theoremdb-0.1.0.tar.gz
  • Upload date:
  • Size: 4.2 kB
  • Tags: Source
  • Uploaded using Trusted Publishing? No
  • Uploaded via: uv/0.11.19 {"installer":{"name":"uv","version":"0.11.19","subcommand":["publish"]},"python":null,"implementation":{"name":null,"version":null},"distro":{"name":"macOS","version":null,"id":null,"libc":null},"system":{"name":null,"release":null},"cpu":null,"openssl_version":null,"setuptools_version":null,"rustc_version":null,"ci":null}

File hashes

Hashes for theoremdb-0.1.0.tar.gz
Algorithm Hash digest
SHA256 63c8e1acf90f011a706a395ee8f2f99a030422b9cda4e6fd131f60ee4c52d5d9
MD5 f6e7eb85f73be024b1dc327851ed3270
BLAKE2b-256 516b090ba2853cf3dea41d7be7a43233a3e960bb640e582b2af082dde8403c3a

See more details on using hashes here.

File details

Details for the file theoremdb-0.1.0-py3-none-any.whl.

File metadata

  • Download URL: theoremdb-0.1.0-py3-none-any.whl
  • Upload date:
  • Size: 5.6 kB
  • Tags: Python 3
  • Uploaded using Trusted Publishing? No
  • Uploaded via: uv/0.11.19 {"installer":{"name":"uv","version":"0.11.19","subcommand":["publish"]},"python":null,"implementation":{"name":null,"version":null},"distro":{"name":"macOS","version":null,"id":null,"libc":null},"system":{"name":null,"release":null},"cpu":null,"openssl_version":null,"setuptools_version":null,"rustc_version":null,"ci":null}

File hashes

Hashes for theoremdb-0.1.0-py3-none-any.whl
Algorithm Hash digest
SHA256 2010354b6a59af74f27e69402cfec58392b4f7c04ca8cee4892b229ad413991a
MD5 18c74f740c5c8fc5e7413ca267c75275
BLAKE2b-256 0cce4992e50c1b579355cf2e06aff791bff199aa7f2f29cf99eec1a0b2825703

See more details on using hashes here.

Supported by

AWS Cloud computing and Security Sponsor Datadog Monitoring Depot Continuous Integration Fastly CDN Google Download Analytics Pingdom Monitoring Sentry Error logging StatusPage Status page