Acornprover

Acorn Theorem Prover Documentation Audit

The docs are unusually thoughtful for a beta theorem prover — a real tutorial arc, a deep language reference, and an ~85-entry library reference — but they are undercut by load-bearing contradictions: the language reference and the library disagree on the name of zero, the one CLI flag the official benchmark blog tells you to run isn't in the CLI reference at all, and several copy-paste examples won't parse as written.

Evidence note: a few findings below (the check flag list, the unbound x/y in the typeclass example, and the == usage) were confirmed from the curator's page annotations because the raw scrapes of those pages were truncated. The quoted text matches the source pages, but the surrounding page bodies were not captured in full.

1. The natural-number zero constructor has two conflicting names (critical)

Location: /docs/language/inductive-types/ and /docs/language/attributes/ vs /docs/library/Nat/

Problem: This is a binary contradiction across two camps. On one side, the Language Reference defines Nat with a base constructor named 0, the attributes page confirms the convention ("Nat.0 is the name for zero, the natural number"), and the induction tutorial writes the base case as plain 0 — these are all the same convention (0 is the numeral name for Nat.0). On the other side, the Library Reference defines the same type as inductive Nat { zero; suc(Nat) } — base constructor zero, i.e. Nat.zero. Worse, the /docs/library/Nat/ page uses both: it declares zero but Nat.0 still appears inside count.

Consequence: A developer (or an AI agent filling in a proof) writing Nat.zero based on the library page hits an undefined name if the kernel expects Nat.0, and vice-versa. There is no note reconciling the two, so the reader cannot tell which is canonical and which is an alias. This is the single most-referenced identifier in every beginner example.

The fix: Pick one canonical spelling, state explicitly that the other is an alias (and where it's valid), and regenerate the Nat library page so it doesn't emit both zero and Nat.0 on the same page.

2. The official benchmark blog tells users to run check --strict, a flag the CLI reference doesn't document (critical)

Location: /blog/freek-top-100/ vs /docs/cli/

Problem: The Freek-100 post instructs: "Acorn's verify command can search for proofs and write certificates, while check --strict must replay committed certificates without performing new search." But the CLI reference documents the check command with only --line and --cert — there is no --strict flag under check. --strict is documented only under verify. (The check flag list is from the curator's annotation on the truncated CLI scrape.)

Consequence: This is precisely the reproducibility workflow the post says CI should use. A developer or automation harness copying check --strict from the official blog either hits an unknown-flag error or silently gets behavior the reference never describes. Because the docs explicitly position the CLI as the surface "useful for automation and agent workflows," this gap breaks exactly the audience it's aimed at.

The fix: If check --strict is real, document the flag under check in the CLI reference (and explain how it differs from verify --strict). If it isn't, correct the blog post to the supported command.

3. Equality is = everywhere except one reference page that uses == (significant)

Location: /docs/language/inductive-types/ vs /docs/language/basic-concepts/

Problem: The basic-concepts reference defines equality as a single =: "An equality is an expression 2 + 2 = 4." Every other language page uses single =. But the inductive-types page's is_three_leaf example uses == (n == 3). (The == usage is from the curator's annotation on the truncated inductive-types scrape.) The docs never state whether == is a distinct boolean operator or a typo — and many provers legitimately have both a propositional = and a boolean ==, so this may be an undocumented feature rather than a broken example.

Consequence: Equality is the most copy-pasted operator in the language. A reader who learns == from the inductive-types example and assumes it works everywhere — or who learns = and is confused by the lone == — has no way to know which the parser accepts, or whether the two mean different things.

The fix: Decide whether =, ==, or both are valid. If only = is valid, fix the is_three_leaf example. If both are valid, document the distinction (propositional vs boolean equality) explicitly on the basic-concepts page instead of silently switching.

4. The discrete typeclass example references unbound variables (significant)

Location: /docs/language/typeclasses/ ("Typeclass Attributes Vs Type Attributes")

Problem: The attributes Color example defines discrete(self, other: Color) but the body tests if x = y — x and y are never bound. The parameters are named self and other. (The unbound x/y is from the curator's annotation on the truncated typeclasses scrape.)

Consequence: The snippet does not compile as printed. A reader copying it to learn the difference between typeclass attributes and type attributes — the entire point of the section — gets an undefined-variable error and is left unsure whether they misunderstood the syntax or the doc is wrong.

The fix: Change the body to reference self and other (e.g. if self = other).

5. The let-satisfy "general form" omits the satisfy keyword every example uses (significant)

Location: /docs/language/functions/ ("Let-satisfy")

Problem: The stated general form is let function_name(...) -> ret: ReturnType { expression } by { proof } — with no satisfy keyword. But every worked example uses it: let predecessor(n: Nat) -> p: Nat satisfy { ... }.

Consequence: The template is the thing a developer copies to write their own definition, and it won't parse — the keyword that names the whole feature is missing from its own syntax skeleton. Readers must reverse-engineer the real syntax from the examples.

The fix: Correct the general form to include satisfy so it matches the examples and actually parses.

6. The nav "GitHub" link points to the math library, not the prover's source (significant)

Location: Homepage nav / footer → https://github.com/acornprover/acornlib

Problem: The single "GitHub" link in the nav and footer goes to acornprover/acornlib. That repo's own README states the language implementation, integrated AI, and VS Code extension live in a separate repo, acornprover/acorn, and the website in a third.

Consequence: A developer clicking "GitHub" to read the prover's source, file a bug against the extension, or understand the AI lands on the math-fact library instead and finds none of it. The actual implementation repo is never linked from the site at all.

The fix: Link the org (github.com/acornprover) or add separate, labeled links for the implementation (acorn), the library (acornlib), and the site.

7. There is no version number anywhere a user installs — it only exists, fragmented, in the blog (significant)

Location: /docs/installation/ and /docs/cli/ vs /blog/

Problem: The install and CLI pages carry no version information. Versions surface only scattered across blog posts — 0.0.5 (generics), 0.0.8 (build cache), 0.1 (certificates), 0.1.8 (square brackets) — and the acornlib GitHub page says "No releases published."

Consequence: A developer can't tell which version the docs describe, whether their installed extension matches, or what changed between versions. With no releases published and version notes buried in prose blog posts, there is no changelog a human or agent can diff against to know if an example still applies.

The fix: Surface the current version on the install page, publish tagged releases, and add a single changelog page instead of leaving the timeline scattered through the blog.

8. The angle-bracket → square-bracket migration is documented only in a blog post (significant)

Location: /blog/square-brackets/ vs /docs/language/generics/

Problem: Every reference page now shows square-bracket type parameters (structure LatticePoint[T], inductive List[T]). The blog post explains that angle brackets (<T>) are still supported but being deprecated since 0.1.8. No reference page mentions the legacy <T> syntax or that it's deprecated.

Consequence: A developer reading existing Acorn code that still uses <T> — which the language still accepts — finds zero explanation in the reference and may assume it's invalid. The deprecation timeline lives only in a dated blog post most readers won't find.

The fix: Add a short note to the generics reference page documenting that <T> is the legacy form, still supported, and slated for deprecation, with a pointer to the migration.

9. Auto-generated library pages leak circular entries, internal aliases, and undocumented notation (significant)

Location: /docs/library/Nat/, /docs/library/List/, /docs/library/Real/

Problem: Generated reference entries are uninformative or expose internals: Nat documents binom as let binom = binom (circular) and mod as let mod = nat_mod (an internal alias with no signature); Real lists let ext = real_ext and let from_rat = real_from_rat with no signatures; List surfaces the internal match representation List.match: (List[T*], R*, (T*, List[T*]) -> R*) -> R* with T*/R* notation that is never defined anywhere in the docs.

Consequence: These pages are the API reference for the library. An entry like let binom = binom tells a developer nothing about arity, arguments, or behavior, and T*/R* reads as a typo or corruption to anyone who hasn't seen it explained (it isn't). The doc generator is publishing implementation noise as public reference.

The fix: Filter circular/alias-only entries out of generated output (or render their real signatures), and either suppress the internal match form or document the T*/R* notation once in a reference legend.

10. The tutorial's documented squiggle outcomes may not reproduce across versions (significant)

Location: /docs/tutorial/multi-step-proofs/, /docs/tutorial/induction/, /docs/tutorial/indirect-proofs/

Problem: The tutorial arc is AI-driven, and the docs themselves flag that its outcomes are unstable. Multi-step-proofs says "Once the AI gets better, we'll have to update this tutorial with a harder theorem!" — i.e. the yellow-squiggle result it shows is tied to the current AI. The induction page shows a Nat.induction example explicitly flagged as non-compiling. Indirect-proofs admits its own approach is questionable ("Using the division theorem is cheating!"). None of these pages state which Acorn/AI version the documented behavior was captured against.

Consequence: A learner following the tutorial expects the same red/yellow-squiggle outcome the page shows. Because proof search is AI-driven and version-dependent, a different installed version can mark a different set of statements as needing detail — so the tutorial's core teaching signal (which steps the AI accepts) can silently diverge from what the reader sees, with no version anchor to explain why.

The fix: Pin each tutorial outcome to a stated Acorn/extension version, and add a short caveat that squiggle results depend on the bundled AI and may differ across versions. Keep a non-AI-dependent fallback example for the steps that must reproduce.

11. The Master Plan page promises a diagram that isn't there (minor)

Location: /docs/tutorial/master-plan/ ("TLDR")

Problem: The project's flagship vision page reads "Here's the plan in diagram form:" and is then followed by no diagram in the rendered content — a missing or inaccessible image at exactly the spot the text points to.

Consequence: The TLDR is the one section meant to convey the whole strategy at a glance, and it resolves to a dangling sentence with nothing after it. A reader who came for the summary gets a broken promise on the page Acorn uses to explain why the project exists.

The fix: Restore the diagram (or remove the "in diagram form" framing and replace it with the text summary the image was meant to carry).

12. The install page silently excludes Intel Macs and omits the CLI install path (minor)

Location: /docs/installation/

Problem: Supported platforms are stated informally as "Windows, Linux, or modern Macs with an M-something chip." "An M-something chip" silently excludes Intel Macs, and the page never mentions that a CLI install path exists on the separate /docs/cli/ page.

Consequence: An Intel-Mac user can't tell whether they're unsupported or just unmentioned, and a developer who wants the CLI for automation won't discover it from the page titled "Installing Acorn."

The fix: State the macOS requirement precisely (Apple Silicon only, and whether Intel/Rosetta works), and link the CLI install instructions from the install page.

13. The CLI docs example's comment contradicts the command it annotates (minor)

Location: /docs/cli/

Problem: The docs example comment says "Generate documentation in the ./docs directory," but the command shown is acorn docs ./docs/library.

Consequence: A reader can't tell whether output lands in ./docs or ./docs/library, and may overwrite the wrong directory or misconfigure automation that depends on the path.

The fix: Make the comment and the path match.

14. Leftover Docusaurus starter scaffolding is live and indexed (minor)

Location: /markdown-page/

Problem: The default Docusaurus template page is still published, with placeholder body "You don't need React to write simple standalone pages." It isn't in the nav but is publicly reachable and in the sitemap.

Consequence: It pollutes search/indexing and signals an unfinished site to anyone (or any crawler) that lands on it.

The fix: Delete the page or exclude it from the build and sitemap.

15. The official blog routes readers to off-site domains for the benchmark and contact (minor)

Location: /blog/freek-top-100/

Problem: The Freek-100 post — published on the official acornprover.org blog as a guest post from "OmegaCombinator Lab" — directs readers to external domains for the canonical results: "The results are tracked publicly at 100.aixmath.org, with the broader AI x Math portal at aixmath.org," alongside blog.aixmath.org and an external contact email.

Consequence: The authoritative status of an official-blog benchmark now depends on third-party domains the project doesn't appear to control. If any of those move or lapse, the post's primary references break, and a reader can't tell where the canonical Acorn benchmark actually lives.

The fix: Mirror or summarize the benchmark results on acornprover.org and clearly mark the guest-post external links as third-party, so the official surface isn't dependent on outside domains for its own data.

16. No llms.txt or machine-readable doc index for a tool that markets agent workflows (minor)

Location: Site root / nav / footer (homepage) — recommendation

Problem: Nothing in the provided nav, footer, or sitemap surfaces an llms.txt/llms-full.txt or any machine-readable index, even though the CLI page explicitly pitches itself as "useful for automation and agent workflows" and the acornlib README invites AI contributions via Codex. (Caveat: an llms.txt conventionally lives at /llms.txt and would not appear in nav/footer — this finding was not verified by fetching acornprover.org/llms.txt directly, so it is framed as a recommendation, not a confirmed 404.)

Consequence: If no such index exists, the product courts AI-agent consumers but offers them only prose pages to crawl, with no consolidated entry point to efficiently locate the language reference, CLI flags, or library signatures — the same surfaces that already contain the contradictions above.

The fix: Confirm whether /llms.txt exists; if not, publish an llms.txt pointing to the key reference pages (language reference, CLI, library index), and ideally an llms-full.txt concatenation, so agents index the docs deterministically.

What they do well

• A genuine tutorial arc (proving a theorem → multi-step → induction → indirect proofs) that teaches the red/yellow-squiggle workflow rather than just dumping syntax — though, per finding #10, its AI-dependent outcomes need version anchoring.
• An honest "Non-features" / experimental section that openly flags unstable features (read, solve, axiom) and admits design choices may change — rare candor for a beta.
• Broad, deep library reference (~85 typeclasses/types spanning algebra and category theory), auto-generated so coverage scales with the library.

Top 3 recommendations

1. Resolve the identifier contradiction first — pick a canonical spelling for the Nat zero constructor (Nat.0 vs Nat.zero), state which is the alias, and regenerate the Nat library page that currently emits both. This breaks the most-copied example in the docs.
2. Make the CLI reference authoritative and the examples copy-pasteable — document every flag the official blog tells users to run (check --strict), and fix the snippets that won't parse (typeclass discrete body, let-satisfy general form, docs path).
3. Surface versioning across the docs, not just the blog — publish tagged releases, show the current version on the install page, version-pin the tutorial outcomes, and document the <T>→[T] migration in the language reference instead of only in a dated post.