Mod-2 Steenrod algebra

Adem reductions as visual proof objects.

The workbench rewrites products of Steenrod squares into the Serre-Cartan admissible basis and exposes every local Adem move, parity decision, cancellation, and compressed graph structure.

SqaSqb=∑j=0⌊a/2⌋(b−j−1a−2j)Sqa+b−jSqj(mod2)Sq^a Sq^b = \sum_{j=0}^{\lfloor a/2 \rfloor}\binom{b-j-1}{a-2j}Sq^{a+b-j}Sq^j \pmod 2
Parsed notation preview
Sq2Sq4Sq2Sq^{2}Sq^{4}Sq^{2}
Example libraryChoose a computation shape
Concept lab

Follow the computation like a machine you can inspect.

Each stage is clickable. The same current trace is interpreted as grammar repair, route splitting, binary filtering, graph compression, and final basis filing.

Raw expression

Input product

The parser turns the user's product of Steenrod squares into monomials that the rewrite engine can inspect.

Like a sentence whose words are in the wrong grammar order.
Mathematical toolchain

Connect Adem reductions to the computational topology ecosystem.

AdemScope should not pretend to replace serious mathematical software. It should become the visual proof and translation layer between Steenrod algebra calculations, homological algebra, computed spaces, spectral sequence workflows, and formal proof certificates.

implemented bridge

SageMath

Cross-check normal forms, compare Serre-Cartan and Milnor bases, export change-of-basis evidence.

Click a trace result, ask Sage for the same basis coordinates, then display agreement or convention mismatch as a visual certificate.
Open source docs
AdemScopeSq-normal form
Current bridgebasis matrix

Steenrod algebra oracle

Workflow lensVerify a published calculation
InputAdemScope trace
→
1normalize
→
2Sage compare
→
3certificate
→
4LaTeX
→
Outputauditable calculation appendix
Connection matrix

Bright cells are not promises of completed integration. They are the most plausible interfaces: traces to Sage, bases to spectral sequence tools, homology to CHomP/Kenzo/HAP-style systems, and certificates toward formal proof environments.

Visual proof explorer

The computation is readable as a flow, a graph, and a basis map.

Run a computation to populate the visual proof explorer.
Expansion frontier

Beyond the calculator.

The strongest direction is a verified rewrite graph workbench with Sage comparison, proof certificates, basis conversion, corpus generation, and eventually odd-prime and cochain-level modules.

Interactive roadmapStage 1 — Correct + Inspectable

Typed algebra core, parser grammar, Sq^0 / zero semantics, deterministic ordering, trace recording, pretty + LaTeX output.

Conference demo targetvisual proof replay
1Trace
2Verify
3Convert
4Atlas
5Discover
6Formalize
Odd-prime scaffold
Research questionsQ1

Which reduction strategy minimizes intermediate support size?