Proof Writing

Helper functions to write proofs in a natural language.

class ProofSections(**data)

Bases: BaseModel

Create a new model by parsing and validating input data from keyword arguments.

Raises [ValidationError][pydantic_core.ValidationError] if the input data cannot be validated to form a valid model.

self is explicitly positional-only to allow self as a field name.

points: list[str]

assumptions: list[str]

numerical_checks: list[str]

trivial_predicates: list[str]

proven_goals: list[str]

unproven_goals: list[str]

proof_steps: list[str]

appendix_ar: list[str]

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

write_proof(proof_data)

Output the solution to out_file.

Parameters:

• proof_state – Proof state.

• problem – Containing the problem definition and theorems.

• out_file – file to write to, empty string to skip writing to file.

Return type:

str

write_proof_sections(proof_data)

Return type:

ProofSections

class CarryOver(carry_over=None)

Bases: object

update(ar_premise)

Return type:

CarryOver