Backbuild Science

Backbuild Science is the research and publishing edition of Backbuild. It is not a separate application: it is a research entitlement layered on the free Backbuild workspace. You write your manuscript in a WYSIWYG editor whose native format is LaTeX, keep your data and figures in the same project, machine-check the mathematics behind your results, and export everything in open, submission-ready formats. Verified students and faculty use all of it at no cost.

Free for current students and faculty. Verify a valid student or faculty ID and Backbuild Science is free, and stays free for 6 months after your ID expires. After that a graduate discount ladder eases you toward the standard Individual rate. Everyone else pays per seat, with Team, Business, and Enterprise plans for labs, departments, and institutions. See Academic Status & Verification and pricing.

A left-to-right flow inside a single dashed project boundary. Stage 1 Author uses Backbuild Docs, Sheets and Slides for the manuscript, data and figures. Stage 2 Verify uses the proof system checked by the kernel. Stage 3 Export produces LaTeX for submission and SQLite for reproducibility. Stage 4 Share uses co-authors and scoped, expiring links. A caption notes that nothing leaves the workspace to move between stages: the manuscript, the data and the proofs stay in one project.
The manuscript, the data, and the proofs stay in one project through every stage, so nothing is exported and re-imported just to move your work forward.

What Backbuild Science adds

The everyday editors (Backbuild Docs, Backbuild Sheets, and Backbuild Slides) are part of the free Backbuild workspace and are available on every plan. Backbuild Science layers the research-grade capabilities on top of them:

WYSIWYG LaTeX authoring

Write mathematics and structured documents in a formatted editor whose source of truth is LaTeX. Toggle to an editable source view (including the preamble) or a side-by-side split at any time, with live math and no compile wait. See the Backbuild Docs editor.

Submission-ready export

Export LaTeX straight from your manuscript for arXiv, journals, and camera-ready builds, and export your Sheets data as a portable SQLite database for reproducibility (Parquet coming soon). See Research authoring & export.

The proof system

Machine-check the theorems and derivations behind your results with a UI-based proof system, backed by a small higher-order-logic (HOL) kernel, and embed a verified result directly in your manuscript. See The proof system.

AI research assistant

Draft, rewrite, translate, and answer questions grounded in your own text. AI usage is not bundled: it runs on your own AI provider keys or on universal usage credits, on every tier including the free Academic tier.

One governed workspace

Manuscript, data, figures, proofs, references, and co-authors live in a single project with scoped sharing, revocable links, role-based access, and audit logs. See Collaborating & sharing research.

HOL kernel & IDE extension

The HOL kernel and the editor IDE extension are unlocked by either Backbuild Science or Backbuild Prove. In Science you use them to verify mathematics; in Prove you use them to verify source code.

How a research project fits together

A research project moves through four stages, all inside one workspace, so your manuscript never drifts out of sync with the data and proofs behind it:

  1. Author. Write your manuscript in Backbuild Docs with live LaTeX, organize datasets and analysis in Backbuild Sheets, and build talks and posters in Backbuild Slides.
  2. Verify. Capture the theorems and derivations as proof entries and check them against the HOL kernel, then reference a verified result from the manuscript.
  3. Export. Produce submission-ready LaTeX from Docs and a portable SQLite database from Sheets, ready to hand to a journal, a preprint server, or a reviewer.
  4. Share. Invite co-authors, control exactly who can see unpublished work, and send a reviewer an expiring, revocable link, all bounded by your organization's sharing rules.

Who Backbuild Science is for

  • Graduate students and PhD candidates writing math-heavy papers, theses, and problem sets who want LaTeX without the compile wall, and free access while they study.
  • Postdocs and early-career researchers who need one place for manuscript, data, figures, and references, and reproducible exports that satisfy funder data-availability mandates.
  • Principal investigators and lab heads standardizing a lab on one collaborative, governed environment with free verified-student seats and no data lock-in.
  • Formal-methods researchers and mathematicians who want machine-checked proofs on a small trusted kernel, embedded directly in the papers that cite them.

Next steps