Legal

Terms and licence

Short version: the papers are open-access and citable; this site's own material is not licensed for reuse; and nothing here is a claim that BSD has been proved.

Last updated 20 October 2026.

Licence

Papers I–IV are deposited open-access on Zenodo under Creative Commons Attribution 4.0 International (CC BY 4.0), each with a citable DOI. The authoritative copy of any paper is its Zenodo deposit.

Everything else on this site is © Damjan Penchev, all rights reserved. That covers the written text, the architecture graph — its structure, statuses, node selection and references — and the presentation of the programme as a whole. It is published to be read and cited, not licensed for reuse.

What you may do without asking

Read, link to, bookmark and cite any page.
Quote short passages for review, criticism, teaching or scholarship, crediting Damjan Penchev and linking to the source.
Redistribute the papers under CC BY 4.0 — that licence is theirs and is unaffected by this page.

Reproducing the architecture graph or substantial parts of the text elsewhere needs permission. Ask at damjanpenchev@proton.me; it is usually given.

The Lean substrate is published in its own repository under the licence stated there, which governs that code regardless of anything on this page.

Status of the mathematics

This is a research programme in progress. Nothing on this site asserts that the Birch and Swinnerton-Dyer conjecture has been proved, and nothing here should be read as a claim of priority over any result it does not itself establish.

The statuses shown on the architecture graph are definitional, not evaluative. They record how far each part has been written down and mechanically checked — not whether it has been reviewed by anyone, and not whether it is correct. In particular:

Established means published in the papers, not independently verified.
Defined means written down and internally consistent — not reviewed, not machine-checked.
Conditional means it depends on a named hypothesis that remains open.
Lean-verified means a machine check passes over the formalised statement, which is a claim about the formalisation and not about the informal mathematics around it.

No part of this work has been peer-reviewed. It should be read as a preprint programme.

Using the site

The site is offered as-is, with no warranty of availability, accuracy or fitness for any purpose, and no liability is accepted for decisions taken on the basis of it. You may read, cite, link to and crawl it. Automated access is welcome within reason — do not degrade the service for others.

Correspondence should be sent to damjanpenchev@proton.me.

Indexing and machine reading

Indexing and archiving are welcome. Search engines, scholarly indexes and web archives may crawl, index, cache and link to this site, and may show short extracts in results. The work exists to be found.

Rights in respect of text and data mining, including the use of this material to train or fine-tune machine-learning models, are expressly reserved under Article 4(3) of Directive (EU) 2019/790. Mining for non-commercial scholarly research under Article 3 is unaffected. For anything else, ask at damjanpenchev@proton.me.

Governing law

These terms are governed by Bulgarian law and, where applicable, by European Union law.