Pith. sign in

REVIEW 1 cited by

Python client for Isabelle server

Not yet reviewed by Pith; the record is open.

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2212.11173 v1 pith:GU3BQJSH submitted 2022-12-09 cs.LO

classification cs.LO
keywords pythonclientisabelleserverdevelopmentscriptannouncementappeared
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

We contribute a Python client for the Isabelle server, which gives researchers and students using Python as their primary programming language an opportunity to communicate with the Isabelle server through TCP directly from a Python script. Such an approach helps avoid the complexities of integrating the existing Python script with languages used for Isabelle development (ML and Scala). We also describe new features that appeared since the announcement of the first version of the client a year ago. Finally, we give examples of the client's applications in research and education and discuss known limitations and possible directions for future development.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. StepProof: Step-by-step verification of natural language mathematical proofs

    cs.LO 2025-06 conditional novelty 5.0 of 10

    Decomposing natural-language proofs into sentence-level formal subproofs improves autoformalization success rates and efficiency compared with whole-proof formalization.

Pith tools