@logos.theorem, logos.check, and logos.prove are the top-level entry points for proof checking.
@logos.theorem — declare a theorem@logos.theorem wraps a function to declare a Theorem object. No proof is run yet.
.proof(...) — attach a proofAttach the proof spec with .proof(tactic1, tactic2, ...). Returns self for chaining:
TrueOr use the decorator form:
logos.check — the compute boundarylogos.check(thm) runs the kernel. Nothing executes until this call:
The proof is a list of tactics applied left-to-right. When a tactic produces subgoals, the next items handle them.
@logos.theorem
def both_positive(x: int, y: int):
return (x > logos.lit(0)) >> ((y > logos.lit(0)) >> ((x > logos.lit(0)) & (y > logos.lit(0))))
logos.check(both_positive.proof(
t.intro("x", "y", "hx", "hy"), # strip foralls and implications
t.split(), # A & B → two subgoals
[t.assumption()], # subgoal 1: x > 0 (in context as hx)
[t.assumption()], # subgoal 2: y > 0 (in context as hy)
))
print("Proved")ProvedLogosProofError is raised with a clear message:
Proof failed: Theorem 'false_claim': ring: Add(left=Var(name='x', type=<class 'int'>), right=Var(name='y', type=<class 'int'>)) ≠ Sub(left=Var(name='x', type=<class 'int'>), right=Var(name='y', type=<class 'int'>)) after normalization
LHS poly: {frozenset({('x', 1)}): 1, frozenset({('y', 1)}): 1}
RHS poly: {frozenset({('x', 1)}): 1, frozenset({('y', 1)}): -1}logos.prove — one-shot anonymous prooflogos.prove(statement, proof_list) creates a _GroundProof — pass it to logos.check():
logos.prove(thm) — automatic proof searchWhen you pass a Theorem object to logos.prove, logos tries to prove it automatically using a cascade of decision procedures: ground computation, polynomial arithmetic, linear arithmetic, and structural decomposition.
TrueThis works for non-trivial goals too. Here is a chain with three quantified variables and two nested hypotheses — logos automatically introduces all variables, collects the hypotheses, and closes with linear arithmetic:
x ≤ y → y ≤ z → x ≤ z ✓For goals that need a conjunction proved, auto splits it and handles each branch separately:
x ≥ 0 → (x+1 ≥ 0) ∧ (x+1 > x) ✓Pass hints to help with defined functions — auto will try unfolding them and then apply arithmetic:
double(double(n)) = 4n ✓Control the search with depth and timeout:
Once a theorem is certified, you can apply it in other proofs using the object directly:
@logos.theorem
def add_comm_v2(x: int, y: int):
return x + y == y + x
logos.check(add_comm_v2.proof(t.intro("x", "y"), t.ring()))
# Use add_comm_v2 as an axiom object in another proof
@logos.theorem
def reorder_sum(x: int, y: int, z: int):
return x + y + z == z + y + x
logos.check(reorder_sum.proof(t.intro("x", "y", "z"), t.ring()))
print("Proved")ProvedA common pattern is a dedicated theorem file that’s imported wherever needed. Since logos.check raises LogosProofError at check time if a proof is wrong, it acts like a compile-time check:
# theorems/arithmetic.py
import logos
import logos.tactics as t
@logos.theorem
def add_comm(x: int, y: int):
return x + y == y + x
logos.check(add_comm.proof(t.intro("x", "y"), t.ring()))
@logos.theorem
def mul_comm(x: int, y: int):
return x * y == y * x
logos.check(mul_comm.proof(t.intro("x", "y"), t.ring()))
# If any proof breaks, this module fails to import.---
title: "Proving Theorems"
---
`@logos.theorem`, `logos.check`, and `logos.prove` are the top-level entry points for proof checking.
## `@logos.theorem` — declare a theorem
`@logos.theorem` wraps a function to declare a `Theorem` object. No proof is run yet.
```{python}
import logos
import logos.tactics as t
@logos.theorem
def add_zero(x: int):
return x + logos.lit(0) == x
print(add_zero) # Theorem[unverified]('add_zero')
print(add_zero.certified) # False — not yet checked
```
## `.proof(...)` — attach a proof
Attach the proof spec with `.proof(tactic1, tactic2, ...)`. Returns `self` for chaining:
```{python}
# Chain style
logos.check(add_zero.proof(t.intro("x"), t.ring()))
print(add_zero.certified) # True
```
Or use the decorator form:
```{python}
@logos.theorem
def add_zero_v2(x: int):
return x + logos.lit(0) == x
@add_zero_v2.proof
def _():
return [t.intro("x"), t.ring()]
logos.check(add_zero_v2)
print("Proved with decorator style")
```
## `logos.check` — the compute boundary
`logos.check(thm)` runs the kernel. Nothing executes until this call:
```{python}
@logos.theorem
def mul_comm(x: int, y: int):
return x * y == y * x
mul_comm.proof(t.intro("x", "y"), t.ring()) # just attaches, doesn't run
logos.check(mul_comm) # NOW it runs
print(mul_comm.certified) # True
```
## The Proof List
The proof is a list of tactics applied left-to-right. When a tactic produces subgoals, the next items handle them.
```{python}
@logos.theorem
def both_positive(x: int, y: int):
return (x > logos.lit(0)) >> ((y > logos.lit(0)) >> ((x > logos.lit(0)) & (y > logos.lit(0))))
logos.check(both_positive.proof(
t.intro("x", "y", "hx", "hy"), # strip foralls and implications
t.split(), # A & B → two subgoals
[t.assumption()], # subgoal 1: x > 0 (in context as hx)
[t.assumption()], # subgoal 2: y > 0 (in context as hy)
))
print("Proved")
```
## What Happens When a Proof Fails
`LogosProofError` is raised with a clear message:
```{python}
from logos.theorem import LogosProofError
@logos.theorem
def false_claim(x: int, y: int):
return x + y == x - y # false!
try:
logos.check(false_claim.proof(t.intro("x", "y"), t.ring()))
except LogosProofError as e:
print(f"Proof failed: {e}")
```
## `logos.prove` — one-shot anonymous proof
`logos.prove(statement, proof_list)` creates a `_GroundProof` — pass it to `logos.check()`:
```{python}
result = logos.check(logos.prove(
logos.forall(int, lambda x: x + logos.lit(0) == x),
[t.intro("x"), t.ring()],
))
print(result.certified) # True
```
## `logos.prove(thm)` — automatic proof search
When you pass a `Theorem` object to `logos.prove`, logos tries to prove it automatically using a cascade of decision procedures: ground computation, polynomial arithmetic, linear arithmetic, and structural decomposition.
```{python}
# No tactic list needed — logos figures it out
@logos.theorem
def add_comm_auto(x: int, y: int):
return x + y == y + x
logos.prove(add_comm_auto)
print(add_comm_auto.certified) # True
```
This works for non-trivial goals too. Here is a chain with three quantified variables and two nested hypotheses — logos automatically introduces all variables, collects the hypotheses, and closes with linear arithmetic:
```{python}
@logos.theorem
def le_trans(x: int, y: int, z: int):
return (x <= y) >> ((y <= z) >> (x <= z))
logos.prove(le_trans)
print("x ≤ y → y ≤ z → x ≤ z ✓")
```
For goals that need a conjunction proved, `auto` splits it and handles each branch separately:
```{python}
@logos.theorem
def nonneg_increment(x: int):
return (x >= logos.lit(0)) >> ((x + logos.lit(1) >= logos.lit(0)) & (x + logos.lit(1) > x))
logos.prove(nonneg_increment)
print("x ≥ 0 → (x+1 ≥ 0) ∧ (x+1 > x) ✓")
```
Pass `hints` to help with defined functions — `auto` will try unfolding them and then apply arithmetic:
```{python}
@logos.define
def double(n: int):
return n + n
@logos.theorem
def double_double(n: int):
return double(double(n)) == logos.lit(4) * n
logos.prove(double_double, hints=[double])
print("double(double(n)) = 4n ✓")
```
Control the search with `depth` and `timeout`:
```python
logos.prove(my_thm, depth=8) # search deeper
logos.prove(my_thm, timeout=2.0) # give up after 2 seconds
```
## Building on Proved Theorems
Once a theorem is certified, you can `apply` it in other proofs using the object directly:
```{python}
@logos.theorem
def add_comm_v2(x: int, y: int):
return x + y == y + x
logos.check(add_comm_v2.proof(t.intro("x", "y"), t.ring()))
# Use add_comm_v2 as an axiom object in another proof
@logos.theorem
def reorder_sum(x: int, y: int, z: int):
return x + y + z == z + y + x
logos.check(reorder_sum.proof(t.intro("x", "y", "z"), t.ring()))
print("Proved")
```
## Module-Level Theorem Files
A common pattern is a dedicated theorem file that's imported wherever needed. Since `logos.check` raises `LogosProofError` at check time if a proof is wrong, it acts like a compile-time check:
```python
# theorems/arithmetic.py
import logos
import logos.tactics as t
@logos.theorem
def add_comm(x: int, y: int):
return x + y == y + x
logos.check(add_comm.proof(t.intro("x", "y"), t.ring()))
@logos.theorem
def mul_comm(x: int, y: int):
return x * y == y * x
logos.check(mul_comm.proof(t.intro("x", "y"), t.ring()))
# If any proof breaks, this module fails to import.
```