diff --git a/M2/Macaulay2/packages/ProofConcept.conversation.md b/M2/Macaulay2/packages/ProofConcept.conversation.md
new file mode 100644
index 00000000000..6f2ac640a45
--- /dev/null
+++ b/M2/Macaulay2/packages/ProofConcept.conversation.md
@@ -0,0 +1,107 @@
+# ProofConcept — design conversation & rationale
+
+This document is the "memory" of the conversation that produced the
+`ProofConcept` package: the original request, how the design evolved, the
+technical findings about Macaulay2 that shaped it, and the decisions made along
+the way. It is a companion to `ProofConcept.m2` and is not loaded by Macaulay2.
+
+## 1. The request
+
+> Create a package `ProofConcept`. We'd like to have data types for
+> * an implication of the type `A => B`;
+> * an atomic proof: a certificate (verifying an implication);
+> * a proof: a collection of implications that prove a given implication.
+
+Three motivating examples were given:
+
+1. **Ideal membership.** `A` = "`G` are generators of an ideal `I` in a
+   polynomial ring and `f` is another polynomial"; `B` = "`f` is in `I`".
+   *Certificate:* polynomials `H` such that `H·G = f`.
+2. **Monomial ideal membership.** Same, but `I` is a monomial ideal.
+   *Certificate:* divisibility of `f` by one of the monomial generators.
+3. **Gröbner basis.** `A` = "`G` generate `I`"; `B` = "`G` is a Gröbner basis
+   with respect to a monomial order". *Proof (non-atomic):* Buchberger's
+   criterion.
+
+## 2. A follow-up that reshaped the design
+
+After the first plan was drafted, the user asked:
+
+> I suppose your suggestion of proof steps just covers a linear chain of
+> implications, correct? Can we add some simple logic (and, or, not, ...) to
+> proofs?
+
+This was the pivotal design change. The initial model had a `Proof` carrying a
+flat list of `Steps` — effectively a linear chain. The revision turns a proof
+into a **tree** whose internal nodes are logical inference rules and whose
+leaves are certificates. Statements become **logical formulas** that can be
+combined with `and`, `or`, `not`.
+
+## 3. Technical findings from exploring Macaulay2
+
+These determined what was idiomatic and feasible:
+
+- **Package skeleton.** `Macaulay2/packages/PackageTemplate.m2` shows the
+  expected shape: `newPackage`, `export`, body, `beginDocumentation()`,
+  `document {…}`, `TEST ///…///`, `end`. New types via `T = new Type of …`;
+  subtypes via `S = new Type of T`.
+- **Membership certificate primitive.** `f // (gens I)` returns the coefficient
+  column `H`, with the identity `f == (gens I)*(f // gens I) + (f % gens I)`
+  (`m2/matrix2.m2`). Membership itself is `f % I == 0` / `isMember(f, I)`.
+- **Monomial ideals.** `MonomialIdeal` is a subtype of `Ideal`, so one
+  `inIdeal(RingElement, Ideal)` constructor covers both; `certify` dispatches
+  separately on `Ideal` vs `MonomialIdeal`.
+- **Faithful Buchberger test.** `forceGB (matrix {G})` wraps the *given*
+  generators as a Gröbner basis so that `S % forceGB …` reduces using only
+  those lead terms. Reducing by `ideal G` directly would always give `0` and
+  prove nothing. S-polynomials are not user-exposed, so they are built by hand
+  from `leadMonomial`, `leadTerm`, and an exponent-vector `lcm`.
+- **Overloadable logical operators.** The interpreter (`d/actors.d`) dispatches
+  `and`/`or`/`not` to installed methods when the operands are *not* Boolean
+  (`binarymethod(…, andS/orS)`, `unarymethod(…, notS)`). So
+  `Statement and Statement`, `Statement or Statement`, and `not Statement`
+  install cleanly with the ordinary `:=` syntax (cf. `m2/integers.m2`:
+  `Function and Function := …`).
+- **`==>` is free.** `==>` is a right-associative binary operator
+  (`d/binding.d`) with no built-in method and a LaTeX rendering of `⟹`, so it
+  is used directly as the implication operator (`A ==> B`).
+
+## 4. Decisions made (with the user)
+
+- **Standalone, not in CI.** The user chose *not* to register the package in
+  `=distributed-packages`, so it is loadable via `loadPackage "ProofConcept"`
+  but is not built/checked in CI. This keeps the proof-of-concept low-risk.
+- **Scope: concept + all three examples.** Core types plus `verify`, with the
+  three worked cases (ideal membership, monomial-ideal membership, Buchberger),
+  documented and tested — rather than a minimal skeleton or a fully extensible
+  certificate framework.
+- **Simple logic, not full natural deduction.** Supported rules are
+  and-introduction, or-introduction, negation certificates, and the derived
+  Buchberger rule. Hypothesis discharge / `or`-elimination case analysis and
+  the `<==>`/`xor` connectives are intentionally left as future work.
+
+## 5. Resulting API
+
+Types: `Statement` (with subtypes `And`, `Or`, `Not`), `Implication`,
+`Certificate`, `Proof`.
+
+- Atomic statements: `inIdeal(f, I)`, `generates(G, I)`, `isGroebner(G)`.
+- Connectives: `A and B`, `A or B`, `not A`; implication `A ==> B`
+  (function form `implies(A, B)`); structural equality `A == B`.
+- Certificate builders: `certify(f, I)` (ideal or monomial-ideal membership),
+  `refute(f, I)` (non-membership, witnessed by the nonzero normal form).
+- Proof-tree builders: `andProof(…)`, `orProof(p, S)`, `buchbergerProof(G)`.
+- Operations: `verify` (independently re-checks the witness in each leaf and
+  the side conditions of each rule, returning a `Boolean`), `conclusion` (the
+  `Statement` a certificate/proof establishes), `proves(P, S)`.
+
+The unifying idea: a proof is *data*, and `verify` re-derives and re-checks it
+rather than trusting how it was produced.
+
+## 6. Status
+
+`ProofConcept.m2` was implemented, documented, and given `TEST` blocks for the
+three cases and the logic layer. No compiled Macaulay2 binary was available in
+the authoring environment, so the package was validated by review; the `TEST`
+blocks are intended to be run with `check ProofConcept` after
+`loadPackage "ProofConcept"` (or `installPackage "ProofConcept"`).
diff --git a/M2/Macaulay2/packages/ProofConcept.m2 b/M2/Macaulay2/packages/ProofConcept.m2
new file mode 100644
index 00000000000..ef64b3a1c0d
--- /dev/null
+++ b/M2/Macaulay2/packages/ProofConcept.m2
@@ -0,0 +1,706 @@
+-- -*- coding: utf-8 -*-
+--		Copyright 2026 by Anton Leykin
+newPackage(
+    "ProofConcept",
+    Version => "0.1",
+    Date => "June 10, 2026",
+    Authors => {
+	{Name => "Anton Leykin", Email => "anton.leykin@gmail.com"}
+	},
+    Headline => "a proof of concept for certificates and proofs of algebraic facts",
+    Keywords => {"Commutative Algebra"},
+    AuxiliaryFiles => false
+    )
+
+-------------------------------------------------------------------------------
+-- This package is a *proof of concept*: it represents simple algebraic facts
+-- as logical statements, and represents proofs of those facts as data that
+-- can be independently re-verified.
+--
+--   * a Statement is a logical formula: an atomic algebraic predicate
+--     (e.g. "f is in the ideal I"), or a compound formula built with the
+--     logical connectives "and", "or", "not";
+--   * an Implication "A ==> B" pairs a hypothesis with a conclusion;
+--   * a Certificate is an *atomic proof*: an algebraic witness whose validity
+--     can be checked cheaply and independently (e.g. the polynomials H with
+--     H*G = f witnessing that f is in the ideal generated by G);
+--   * a Proof is a *tree* of inference steps: leaf Certificates combined by
+--     logical rules (and-introduction, or-introduction) and the derived
+--     Buchberger rule, establishing a goal Statement.
+--
+-- The verb that ties it together is "verify": it recomputes and re-checks
+-- the witness in each leaf and the side conditions of each rule.
+-------------------------------------------------------------------------------
+
+export {
+    -- types
+    "Statement", "And", "Or", "Not", "Implication", "Certificate", "Proof",
+    -- atomic statements
+    "inIdeal", "generates", "isGroebner",
+    -- implication
+    "implies",
+    -- certificate builders
+    "certify", "refute",
+    -- proof-tree builders
+    "andProof", "orProof", "buchbergerProof",
+    -- operations
+    "verify", "conclusion", "proves"
+    }
+
+-------------------------------------------------------------------------------
+-- Types
+-------------------------------------------------------------------------------
+
+Statement   = new Type of HashTable	-- a logical formula
+And         = new Type of Statement	-- conjunction
+Or          = new Type of Statement	-- disjunction
+Not         = new Type of Statement	-- negation
+Implication = new Type of HashTable	-- A ==> B
+Certificate = new Type of HashTable	-- atomic proof (a re-checkable witness)
+Proof       = new Type of HashTable	-- a tree of inference steps
+
+-------------------------------------------------------------------------------
+-- Atomic statements
+-------------------------------------------------------------------------------
+
+inIdeal = method()
+inIdeal(RingElement, Ideal) := (f, I) -> new Statement from {
+    "description" => toString f | " is in the ideal " | toString I,
+    "predicate"   => "InIdeal",
+    "data"        => new HashTable from {"element" => f, "ideal" => I}}
+
+generates = method()
+generates(List, Ideal) := (G, I) -> new Statement from {
+    "description" => toString G | " generate " | toString I,
+    "predicate"   => "Generates",
+    "data"        => new HashTable from {"gens" => G, "ideal" => I}}
+generates(Matrix, Ideal) := (G, I) -> generates(first entries G, I)
+
+isGroebner = method()
+isGroebner List := G -> new Statement from {
+    "description" => toString G | " is a Groebner basis",
+    "predicate"   => "IsGroebner",
+    "data"        => new HashTable from {"gens" => G}}
+isGroebner Matrix := G -> isGroebner first entries G
+
+-------------------------------------------------------------------------------
+-- Logical connectives: and, or, not, and the implication operator ==>
+-------------------------------------------------------------------------------
+
+Statement and Statement := (A, B) -> (
+    aa := if instance(A, And) then A#"args" else {A};
+    bb := if instance(B, And) then B#"args" else {B};
+    new And from {"args" => join(aa, bb)})
+
+Statement or Statement := (A, B) -> (
+    aa := if instance(A, Or) then A#"args" else {A};
+    bb := if instance(B, Or) then B#"args" else {B};
+    new Or from {"args" => join(aa, bb)})
+
+not Statement := A -> (
+    if instance(A, Not) then A#"arg"		-- collapse double negation
+    else new Not from {"arg" => A})
+
+implies = method()
+implies(Statement, Statement) := Implication => (A, B) ->
+    new Implication from {"hyp" => A, "concl" => B}
+
+Statement ==> Statement := (A, B) -> implies(A, B)
+
+-- structural equality of statements (the hash tables are distinct objects,
+-- so === is too strict; we compare structure instead)
+Statement == Statement := (A, B) -> A === B or (
+    class A === class B and (
+	if instance(A, And) or instance(A, Or) then (
+	    la := A#"args"; lb := B#"args";
+	    #la == #lb and all(0 ..< #la, k -> la#k == lb#k))
+	else if instance(A, Not) then A#"arg" == B#"arg"
+	else A#"predicate" == B#"predicate" and A#"description" == B#"description"))
+
+-------------------------------------------------------------------------------
+-- Certificate builders
+-------------------------------------------------------------------------------
+
+-- f in I, with I an ordinary ideal: the witness is the column H of
+-- coefficients satisfying (gens I) * H = f.
+certify = method()
+certify(RingElement, Ideal) := Certificate => (f, I) -> (
+    if f % I != 0 then error "no certificate: the element is not in the ideal";
+    H := f // gens I;
+    new Certificate from {
+	"conclusion" => inIdeal(f, I),
+	"witness"    => H,
+	"strategy"   => "IdealMembership"})
+
+-- f in I, with I a monomial ideal and f a monomial: the witness is a
+-- generator g dividing f together with the quotient monomial q = f/g.
+certify(RingElement, MonomialIdeal) := Certificate => (f, I) -> (
+    if size f != 1 then error "monomial certificate expects a monomial; use certify(f, ideal I) instead";
+    gs := first entries gens I;
+    pos := position(gs, g -> f % g == 0);
+    if pos === null then error "no certificate: no generator divides the element";
+    g := gs#pos;
+    new Certificate from {
+	"conclusion" => inIdeal(f, I),
+	"witness"    => (g, f // g),
+	"strategy"   => "MonomialDivision"})
+
+-- f is NOT in I: the witness is the nonzero normal form f % I.
+refute = method()
+refute(RingElement, Ideal) := Certificate => (f, I) -> (
+    r := f % I;
+    if r == 0 then error "cannot refute: the element is in the ideal";
+    new Certificate from {
+	"conclusion" => not inIdeal(f, I),
+	"witness"    => r,
+	"strategy"   => "NonMembership"})
+
+-------------------------------------------------------------------------------
+-- Proof-tree builders
+-------------------------------------------------------------------------------
+
+-- lcm of two monomials, via exponent vectors (robust and order-independent)
+lcmMonomial := (a, b) -> (
+    ea := first exponents a;
+    eb := first exponents b;
+    R := ring a;
+    product(numgens R, k -> R_k^(max(ea#k, eb#k))))
+
+-- S-polynomial of two ring elements
+spoly := (gi, gj) -> (
+    gamma := lcmMonomial(leadMonomial gi, leadMonomial gj);
+    (gamma // leadTerm gi) * gi - (gamma // leadTerm gj) * gj)
+
+-- and-introduction: combine proofs of B_1, ..., B_n into a proof of their
+-- conjunction.  Accepts a sequence andProof(p,q,...), a list, or a single proof.
+andProof = ps -> (
+    L := if instance(ps, Sequence) then toList ps
+         else if instance(ps, List) then ps
+	 else {ps};
+    new Proof from {
+	"rule"       => "AndIntro",
+	"subproofs"  => L,
+	"conclusion" => fold((a, b) -> a and b, apply(L, conclusion))})
+
+-- or-introduction: from a proof p of one disjunct, prove the disjunction S.
+orProof = (p, S) -> new Proof from {
+    "rule"       => "OrIntro",
+    "subproofs"  => {p},
+    "conclusion" => S}
+
+-- Buchberger's criterion: G is a Groebner basis iff every S-polynomial of a
+-- pair of generators reduces to zero modulo G.  Each S-polynomial is also
+-- packaged as a membership certificate (it lies in the ideal generated by G).
+buchbergerProof = method()
+buchbergerProof List := Proof => G -> (
+    J := ideal G;
+    certs := flatten for i from 0 to #G - 1 list (
+	for j from i + 1 to #G - 1 list (
+	    if G#i == 0 or G#j == 0 then continue;
+	    certify(spoly(G#i, G#j), J)));
+    new Proof from {
+	"rule"       => "Buchberger",
+	"subproofs"  => certs,
+	"conclusion" => isGroebner G,
+	"gens"       => G})
+buchbergerProof Ideal  := Proof => I -> buchbergerProof first entries gens I
+buchbergerProof Matrix := Proof => G -> buchbergerProof first entries G
+
+-------------------------------------------------------------------------------
+-- conclusion: the Statement that a certificate or proof establishes
+-------------------------------------------------------------------------------
+
+conclusion = method()
+conclusion Certificate := Statement => c -> c#"conclusion"
+conclusion Proof       := Statement => p -> p#"conclusion"
+
+-------------------------------------------------------------------------------
+-- verify: independently re-check a certificate or proof, returning a Boolean
+-------------------------------------------------------------------------------
+
+verify = method()
+verify Certificate := Boolean => c -> (
+    strat := c#"strategy";
+    st := c#"conclusion";
+    if strat == "IdealMembership" then (
+	f := st#"data"#"element";
+	I := st#"data"#"ideal";
+	H := c#"witness";
+	(gens I * H)_(0,0) == f)
+    else if strat == "MonomialDivision" then (
+	f := st#"data"#"element";
+	I := st#"data"#"ideal";
+	(g, q) := c#"witness";
+	any(first entries gens I, h -> h == g) and q * g == f)
+    else if strat == "NonMembership" then (
+	-- st is a Not whose argument is the membership statement
+	inner := st#"arg";
+	f := inner#"data"#"element";
+	I := inner#"data"#"ideal";
+	f % I != 0 and c#"witness" == f % I)
+    else error("unknown certificate strategy: " | toString strat))
+
+verify Proof := Boolean => p -> (
+    rule := p#"rule";
+    if rule == "AndIntro" then
+	all(p#"subproofs", verify)
+    else if rule == "OrIntro" then (
+	sub := first p#"subproofs";
+	S := p#"conclusion";
+	verify sub and instance(S, Or) and any(S#"args", d -> d == conclusion sub))
+    else if rule == "Buchberger" then (
+	G := p#"gens";
+	GG := forceGB matrix {G};
+	reduces := all(0 ..< #G, i ->
+	    all(i + 1 ..< #G, j ->
+		G#i == 0 or G#j == 0 or spoly(G#i, G#j) % GG == 0));
+	reduces and all(p#"subproofs", verify))
+    else error("unknown proof rule: " | toString rule))
+
+-- proves(P, S): P verifies and its conclusion is (structurally) S
+proves = method()
+proves(Certificate, Statement) := Boolean => (c, S) -> verify c and conclusion c == S
+proves(Proof,       Statement) := Boolean => (p, S) -> verify p and conclusion p == S
+
+-------------------------------------------------------------------------------
+-- Pretty printing
+-------------------------------------------------------------------------------
+
+net Statement   := S -> net S#"description"
+net And         := S -> horizontalJoin join({"("}, between(" and ", apply(S#"args", net)), {")"})
+net Or          := S -> horizontalJoin join({"("}, between(" or ",  apply(S#"args", net)), {")"})
+net Not         := S -> horizontalJoin {"(not ", net S#"arg", ")"}
+net Implication := P -> horizontalJoin {net P#"hyp", " ==> ", net P#"concl"}
+net Certificate := c -> horizontalJoin {"Certificate of (", net conclusion c, ")"}
+net Proof       := p -> horizontalJoin {"Proof of (", net conclusion p, ") by ", p#"rule"}
+
+-------------------------------------------------------------------------------
+-- Documentation
+-------------------------------------------------------------------------------
+
+beginDocumentation()
+
+document {
+    Key => ProofConcept,
+    Headline => "a proof of concept for certificates and proofs of algebraic facts",
+    PARA {
+	"This package is a ", EM "proof of concept", ".  It represents simple ",
+	"algebraic facts as logical ", TO2 {Statement, "statements"}, ", and ",
+	"represents their proofs as data that can be re-verified independently."
+	},
+    PARA { "The vocabulary is:" },
+    UL {
+	{TO Statement, " -- a logical formula: an atomic algebraic predicate ",
+	    "such as ", TO inIdeal, ", or a compound formula built with the ",
+	    "connectives ", TT "and", ", ", TT "or", ", ", TT "not", "."},
+	{TO Implication, " -- a hypothesis and a conclusion, written ", TT "A ==> B", "."},
+	{TO Certificate, " -- an ", EM "atomic proof", ": a witness whose ",
+	    "validity is checked cheaply and independently."},
+	{TO Proof, " -- a ", EM "tree", " of inference steps combining ",
+	    "certificates by logical rules."},
+	{TO verify, " -- recompute and re-check the witnesses and side conditions."}
+	},
+    PARA { "A first example, ideal membership:" },
+    EXAMPLE lines ///
+	R = QQ[x,y,z];
+	I = ideal(x^2 - y, y^3);
+	c = certify(x^2*y^3, I)
+	verify c
+    ///,
+    PARA { "The Groebner basis property, via Buchberger's criterion:" },
+    EXAMPLE lines ///
+	p = buchbergerProof I
+	verify p
+    ///
+    }
+
+document {
+    Key => Statement,
+    Headline => "a logical statement about algebraic objects",
+    PARA {
+	"A ", TT "Statement", " is an atomic algebraic predicate -- built by ",
+	TO inIdeal, ", ", TO generates, ", or ", TO isGroebner, " -- or a ",
+	"compound formula built from these with ", TT "and", ", ", TT "or", ", ",
+	"and ", TT "not", "."
+	},
+    EXAMPLE lines ///
+	R = QQ[x,y];
+	I = ideal(x^2, y);
+	s = inIdeal(x^2, I)
+	t = inIdeal(y, I)
+	s and t
+	s or (not t)
+    ///,
+    SeeAlso => {And, Or, Not, Implication, inIdeal, generates, isGroebner}
+    }
+
+document {
+    Key => {And, Or, Not},
+    Headline => "compound logical statements",
+    PARA {
+	"These types represent conjunctions, disjunctions, and negations of ",
+	TO2 {Statement, "statements"}, ".  They are produced by the overloaded ",
+	"operators ", TT "and", ", ", TT "or", ", and ", TT "not", "; nested ",
+	TT "and", "/", TT "or", " are flattened and double negations collapse."
+	},
+    EXAMPLE lines ///
+	R = QQ[x,y];
+	I = ideal(x^2, y);
+	(inIdeal(x^2,I) and inIdeal(y,I)) and inIdeal(x^2*y,I)
+	not not inIdeal(y,I)
+    ///,
+    SeeAlso => {Statement}
+    }
+
+document {
+    Key => Implication,
+    Headline => "an implication A ==> B",
+    PARA {
+	"An ", TT "Implication", " pairs a hypothesis statement with a ",
+	"conclusion statement.  It is built with ", TO implies, " or the ",
+	"operator ", TT "==>", "."
+	},
+    EXAMPLE lines ///
+	R = QQ[x,y];
+	I = ideal(x^2, y);
+	generates({x^2, y}, I) ==> inIdeal(x^2*y, I)
+    ///,
+    SeeAlso => {implies}
+    }
+
+document {
+    Key => Certificate,
+    Headline => "an atomic, independently checkable proof",
+    PARA {
+	"A ", TT "Certificate", " is a witness for a single atomic ",
+	TO2 {Statement, "statement"}, ".  It is produced by ", TO certify,
+	" (membership) or ", TO refute, " (non-membership), and re-checked by ",
+	TO verify, "."
+	},
+    EXAMPLE lines ///
+	R = QQ[x,y,z];
+	I = ideal(x^2 - y, y^3);
+	c = certify(x^2*y^3, I)
+	conclusion c
+	verify c
+    ///,
+    SeeAlso => {certify, refute, verify, Proof}
+    }
+
+document {
+    Key => Proof,
+    Headline => "a tree of inference steps",
+    PARA {
+	"A ", TT "Proof", " combines certificates and sub-proofs by logical ",
+	"rules: ", TO andProof, " (and-introduction), ", TO orProof,
+	" (or-introduction), and the derived rule ", TO buchbergerProof, ".  ",
+	TO verify, " re-checks the whole tree."
+	},
+    EXAMPLE lines ///
+	R = QQ[x,y,z];
+	I = ideal(x^2 - y, y^3);
+	c = certify(x^2*y^3, I);
+	d = certify(x^2 - y, I);
+	p = andProof(c, d)
+	verify p
+    ///,
+    SeeAlso => {andProof, orProof, buchbergerProof, verify}
+    }
+
+document {
+    Key => {inIdeal, (inIdeal, RingElement, Ideal)},
+    Headline => "the statement that a polynomial lies in an ideal",
+    Usage => "inIdeal(f, I)",
+    Inputs => {"f" => RingElement, "I" => Ideal},
+    Outputs => {Statement => {"the assertion that ", TT "f", " is in ", TT "I"}},
+    EXAMPLE lines ///
+	R = QQ[x,y];
+	inIdeal(x^2*y, ideal(x^2, y))
+    ///,
+    SeeAlso => {certify, refute}
+    }
+
+document {
+    Key => {generates, (generates, List, Ideal), (generates, Matrix, Ideal)},
+    Headline => "the statement that a set generates an ideal",
+    Usage => "generates(G, I)",
+    Inputs => {"G" => List, "I" => Ideal},
+    Outputs => {Statement},
+    EXAMPLE lines ///
+	R = QQ[x,y];
+	I = ideal(x^2, y);
+	generates({x^2, y}, I)
+    ///
+    }
+
+document {
+    Key => {isGroebner, (isGroebner, List), (isGroebner, Matrix)},
+    Headline => "the statement that a set is a Groebner basis",
+    Usage => "isGroebner G",
+    Inputs => {"G" => List},
+    Outputs => {Statement},
+    EXAMPLE lines ///
+	R = QQ[x,y,z];
+	isGroebner first entries gens gb ideal(x^2 - y, y^3)
+    ///,
+    SeeAlso => {buchbergerProof}
+    }
+
+document {
+    Key => {implies, (implies, Statement, Statement)},
+    Headline => "form an implication",
+    Usage => "implies(A, B)",
+    Inputs => {"A" => Statement, "B" => Statement},
+    Outputs => {Implication},
+    PARA {"The operator ", TT "A ==> B", " is a synonym for ", TT "implies(A, B)", "."},
+    EXAMPLE lines ///
+	R = QQ[x,y];
+	I = ideal(x^2, y);
+	implies(generates({x^2, y}, I), inIdeal(x^2*y, I))
+    ///
+    }
+
+document {
+    Key => {certify, (certify, RingElement, Ideal), (certify, RingElement, MonomialIdeal)},
+    Headline => "build a certificate of ideal membership",
+    Usage => "certify(f, I)",
+    Inputs => {"f" => RingElement, "I" => Ideal},
+    Outputs => {Certificate => {"a witness that ", TT "f", " is in ", TT "I"}},
+    PARA {
+	"For an ordinary ideal the witness is the row ", TT "H", " of ",
+	"coefficients with ", TT "(gens I) * H == f", ".  For a ",
+	TO MonomialIdeal, " and a monomial ", TT "f", " the witness is a ",
+	"generator dividing ", TT "f", " together with the quotient monomial.  ",
+	"An error is raised when ", TT "f", " is not in ", TT "I", "."
+	},
+    EXAMPLE lines ///
+	R = QQ[x,y,z];
+	I = ideal(x^2 - y, y^3);
+	verify certify(x^2*y^3, I)
+	M = monomialIdeal(x^2*y, x*y*z, y^3);
+	verify certify(x^3*y^2, M)
+    ///,
+    SeeAlso => {refute, verify}
+    }
+
+document {
+    Key => {refute, (refute, RingElement, Ideal)},
+    Headline => "build a certificate of non-membership",
+    Usage => "refute(f, I)",
+    Inputs => {"f" => RingElement, "I" => Ideal},
+    Outputs => {Certificate => {"a witness that ", TT "f", " is not in ", TT "I"}},
+    PARA {
+	"The witness is the nonzero normal form ", TT "f % I", ".  The ",
+	"conclusion is the negated statement ", TT "not inIdeal(f, I)", "."
+	},
+    EXAMPLE lines ///
+	R = QQ[x,y,z];
+	I = ideal(x^2 - y, y^3);
+	c = refute(x, I)
+	verify c
+    ///,
+    SeeAlso => {certify}
+    }
+
+document {
+    Key => andProof,
+    Headline => "and-introduction: prove a conjunction",
+    Usage => "andProof(p, q, ...)",
+    PARA {
+	"Combines proofs (or certificates) of statements ", TT "B_1, ..., B_n",
+	" into a ", TO Proof, " of their conjunction.  Accepts a sequence, a ",
+	"list, or a single proof."
+	},
+    EXAMPLE lines ///
+	R = QQ[x,y,z];
+	I = ideal(x^2 - y, y^3);
+	p = andProof(certify(x^2*y^3, I), certify(x^2 - y, I));
+	conclusion p
+	verify p
+    ///,
+    SeeAlso => {orProof, verify}
+    }
+
+document {
+    Key => orProof,
+    Headline => "or-introduction: prove a disjunction",
+    Usage => "orProof(p, S)",
+    PARA {
+	"From a proof ", TT "p", " of one disjunct, builds a ", TO Proof,
+	" of the disjunction ", TT "S", ".  Verification checks that the ",
+	"conclusion of ", TT "p", " is one of the disjuncts of ", TT "S", "."
+	},
+    EXAMPLE lines ///
+	R = QQ[x,y,z];
+	I = ideal(x^2 - y, y^3);
+	c = certify(x^2*y^3, I);
+	S = conclusion c or inIdeal(x, I);
+	verify orProof(c, S)
+    ///,
+    SeeAlso => {andProof, verify}
+    }
+
+document {
+    Key => {buchbergerProof, (buchbergerProof, List), (buchbergerProof, Ideal), (buchbergerProof, Matrix)},
+    Headline => "prove that a set is a Groebner basis via Buchberger's criterion",
+    Usage => "buchbergerProof G",
+    Inputs => {"G" => {ofClass List, ", ", ofClass Ideal, ", or ", ofClass Matrix}},
+    Outputs => {Proof => {"a proof that ", TT "G", " is a Groebner basis"}},
+    PARA {
+	"Builds the proof tree whose leaves assert, for each pair of generators, ",
+	"that the corresponding S-polynomial lies in the ideal.  ", TO verify,
+	" checks Buchberger's criterion: every S-polynomial reduces to zero ",
+	"modulo ", TT "G", " (using only the lead terms of ", TT "G", ").  ",
+	"If ", TT "G", " is not a Groebner basis, ", TO verify, " returns ",
+	TT "false", "."
+	},
+    EXAMPLE lines ///
+	R = QQ[x,y,z];
+	I = ideal(x^2 - y, y^3);
+	G = first entries gens gb I;
+	verify buchbergerProof G
+	verify buchbergerProof {x^3 - 2*x*y, x^2*y - 2*y^2 + x}
+    ///,
+    SeeAlso => {isGroebner, verify}
+    }
+
+document {
+    Key => {verify, (verify, Certificate), (verify, Proof)},
+    Headline => "independently re-check a certificate or proof",
+    Usage => "verify c",
+    Inputs => {"c" => {ofClass Certificate, " or ", ofClass Proof}},
+    Outputs => {Boolean},
+    PARA {
+	"Recomputes the witness in each leaf certificate and the side ",
+	"conditions of each rule, returning ", TT "true", " only if everything ",
+	"checks out.  This is independent of how the certificate or proof was ",
+	"produced."
+	},
+    EXAMPLE lines ///
+	R = QQ[x,y,z];
+	I = ideal(x^2 - y, y^3);
+	verify certify(x^2*y^3, I)
+    ///,
+    SeeAlso => {certify, refute, proves}
+    }
+
+document {
+    Key => {conclusion, (conclusion, Certificate), (conclusion, Proof)},
+    Headline => "the statement established by a certificate or proof",
+    Usage => "conclusion c",
+    Inputs => {"c" => {ofClass Certificate, " or ", ofClass Proof}},
+    Outputs => {Statement},
+    EXAMPLE lines ///
+	R = QQ[x,y,z];
+	I = ideal(x^2 - y, y^3);
+	conclusion certify(x^2*y^3, I)
+    ///,
+    SeeAlso => {verify, proves}
+    }
+
+document {
+    Key => {proves, (proves, Certificate, Statement), (proves, Proof, Statement)},
+    Headline => "test whether a certificate or proof establishes a given statement",
+    Usage => "proves(c, S)",
+    Inputs => {"c" => {ofClass Certificate, " or ", ofClass Proof}, "S" => Statement},
+    Outputs => {Boolean => {TT "c", " verifies and its conclusion is ", TT "S"}},
+    EXAMPLE lines ///
+	R = QQ[x,y,z];
+	I = ideal(x^2 - y, y^3);
+	c = certify(x^2*y^3, I);
+	proves(c, inIdeal(x^2*y^3, I))
+    ///,
+    SeeAlso => {verify, conclusion}
+    }
+
+-------------------------------------------------------------------------------
+-- Tests
+-------------------------------------------------------------------------------
+
+TEST ///
+  -- (1) ideal membership certificate
+  R = QQ[x,y,z];
+  I = ideal(x^2 - y, y^3);
+  f = x^2*y^3;
+  c = certify(f, I);
+  assert(class c === Certificate);
+  assert(verify c);
+  assert(conclusion c == inIdeal(f, I));
+  assert(proves(c, inIdeal(f, I)));
+  -- the witness really satisfies (gens I) * H == f
+  H = c#"witness";
+  assert((gens I * H)_(0,0) == f);
+  -- certify errors when f is not in I
+  assert(try (certify(x, I); false) else true);
+///
+
+TEST ///
+  -- (2) monomial ideal membership certificate
+  R = QQ[x,y,z];
+  M = monomialIdeal(x^2*y, x*y*z, y^3);
+  c = certify(x^3*y^2, M);
+  assert(verify c);
+  (g, q) = c#"witness";
+  assert(q * g == x^3*y^2);
+  assert(any(first entries gens M, h -> h == g));
+///
+
+TEST ///
+  -- (3) Buchberger proof that a Groebner basis is a Groebner basis
+  R = QQ[x,y,z];
+  I = ideal(x^2 - y, y^3);
+  G = first entries gens gb I;
+  p = buchbergerProof G;
+  assert(class p === Proof);
+  assert(verify p);
+  assert(conclusion p == isGroebner G);
+  -- a non-Groebner generating set (its S-polynomial reduces to -x^2 =!= 0)
+  q = buchbergerProof {x^3 - 2*x*y, x^2*y - 2*y^2 + x};
+  assert(not verify q);
+///
+
+TEST ///
+  -- non-membership (negation) certificates
+  R = QQ[x,y,z];
+  I = ideal(x^2 - y, y^3);
+  c = refute(x, I);
+  assert(verify c);
+  assert(instance(conclusion c, Not));
+  assert(try (refute(x^2*y^3, I); false) else true);
+///
+
+TEST ///
+  -- the logic layer: connectives build the right types and flatten/collapse
+  R = QQ[x,y];
+  I = ideal(x^2, y);
+  s = inIdeal(x^2, I);
+  t = inIdeal(y, I);
+  assert(instance(s and t, And));
+  assert(instance(s or t, Or));
+  assert(instance(not s, Not));
+  assert((not not s) == s);			-- double negation collapses
+  assert(#(((s and t) and s)#"args") == 3);	-- nested and flattens
+  assert(instance(s ==> t, Implication));
+///
+
+TEST ///
+  -- proof-tree combinators: and-introduction and or-introduction
+  R = QQ[x,y,z];
+  I = ideal(x^2 - y, y^3);
+  c = certify(x^2*y^3, I);
+  d = certify(x^2 - y, I);
+  p = andProof(c, d);
+  assert(verify p);
+  assert(conclusion p == (inIdeal(x^2*y^3, I) and inIdeal(x^2 - y, I)));
+  -- or-introduction from one true disjunct
+  S = conclusion c or inIdeal(x, I);
+  assert(verify orProof(c, S));
+///
+
+end
+
+-- Development scratch: none of this runs on load (stops at "end").
+restart
+loadPackage("ProofConcept", FileName => "ProofConcept.m2")
+check ProofConcept
+installPackage "ProofConcept"