Help

A network of statements. Every definition, lemma and theorem is a node; every use of one by another is an edge. That is the whole artifact — there is no accompanying document, and no PDF stage anywhere in the process.

The claim behind that is narrow and testable: almost everything a preprint does for a reader is done better by the network, and the one thing a document does that a network cannot — read straight through — is served by writing the narrative as prose that embeds the statements, which is what a topic in a vault is.

1. 1
   Write

   A vault of Markdown, one file per statement and one per edge. Obsidian opens it; so does anything else.

2. 2
   Compile

   The vault becomes a network: every definition and theorem a node, every use of one by another an edge.

3. 3
   Pool

   Networks merge by content address. A statement two subjects share is stored once, and the merge needs nobody’s agreement.

4. 4
   Formalize

   A proof assistant reads the pool for its semantics — what depends on what, and what a name was meant to mean.

A card’s address is a hash of its statement, so two people who state the same thing produce the same address without coordinating. Merging two networks is then a set union: no reconciliation step, no authority deciding whose version of a definition wins, and no possibility of the same statement appearing twice under different names.

It has a cost, and it is worth knowing before you write: editing a statement changes its address. Proofs, notes and titles do not — only the statement itself. Links people saved to an edited statement break, which is why a network that is still moving should stay in draft.

That a subject arrived sharing no statement with anything already here. Two components is the normal state of a young pool, not a defect — they join when something is proved that uses both sides, and until then the count is an honest measure of how far apart the subjects are.

A repository shaped like the vault template: a curated pool of cards under <Name>Hypergraph/, narratives under topics/, a bibliography, and tools/. Starting from the template is the easy path — gh repo create … --template AstrolabeNet-Temp then python3 tools/init.py <Name>.

That the network compiles and displays: every link resolves, every edge has two ends that exist, every card is addressable, every figure is in the repository, and the mathematics renders. Each of those answers “what breaks on the page if this is wrong?”, and a rule with no answer to that is not this site’s business.

Your vault’s own tools/ are deliberately not run here. Most of what they check is one vault’s house style, and a submitter shipping weakened linters would pass their own bar — the bar has to be held by the side accepting. Run them yourself; they catch far more than this does.

It is the same kind of criterion as “it has to compile to a PDF”: mechanical, checkable before submitting, and about form rather than about whether the mathematics is any good. Nobody here judges the latter.

Anyone, for any public repository whose format fits. You do not have to own it. What authorises publishing is the licence, read out of the repository and never chosen on a form — no licence means all rights reserved, which means refused, not because the mathematics is unwelcome but because nobody may redistribute it.

The record keeps no submitter. Credit belongs to whoever wrote the mathematics, and the repository already says who that is: the narrative’s own authors:, then CITATION.cff, then the people who committed to it. Pressing submit is not authorship.

On the submission page: sign in with GitHub, drop in the repository link, and the repository answers for itself — title, sections, licence and shape are all read at the commit being pinned, so there is nothing to fill in and nothing that can drift out of step with the source.

Submitting opens a pull request against this site adding that commit to submissions.json. Merging it publishes. Nothing is stored on the server in between: a pull request is already a queue, already has review, and already has an audit trail.

The site compiles the commit you pinned and no other, so a later push to your repository changes nothing here until you submit again. That is what makes a published entry a fixed thing somebody can cite.

The narratives you name, the cards those narratives embed, one round of the cards their statements cite so terms stay clickable, and the edges between all of those. Nothing else — a card nobody’s narrative reaches never leaves your repository. Proofs and notes travel, folded, as they read in the vault.

Publishing is therefore an act of writing rather than of configuration: a statement appears on this site because a narrative you wrote embeds it.

From your .lean sources, read as text — which reaches about 47% of what your project actually depends on. A lemma reached through open, or one simp found without being told, is not in the text to be read. That is a limit of reading rather than a bug in it, and it is the price of asking nothing of your repository.

You can lift it by publishing what your compiler already knows. Copy templates/astrolabe-ilean.yml into .github/workflows/. It runs lake build and attaches the .ilean files it produces — the ones the language server uses for find-references — to a release tagged with the commit. Your project gets no new Lake target, no dependency on this site, and no secret. The artifact is a couple of hundred kilobytes.

With it the same project reaches 81%, and every name is one the elaborator resolved rather than one we matched. Without it nothing breaks; the network publishes either way.

Neither reading is the proof term. A .ilean reference is a name somebody wrote: a have the final term routes around still counts. Which reading a network used is recorded with it, because two edges look the same on the page and a reader has no other way to tell.