Skip to content
Modern Math
Mailing listLogica Artificialislogicartificialis@googlesites.com
Get in touchlogicartificialis.orglogicartificialis@gmail.com
CompanionDistilled Proofdistilledproof.org

Companions

The project, and a companion

Modern Math is a collaborative project of Logica Artificialis. Distilled Proof remains a neighbouring site. Write through the institute, not through a personal byline.

logicartificialis.org

LogicArtificialis

Artificial logic, made checkable.

LogicArtificialis seal: a corgi and a capybara sit beside a sapphire held in a turtle, with the turnstile cut into the stone. The ring reads Organum rationis, sapphirus mentis.
The seal. Corgi and capybara, the turtle, the sapphire, and the turnstile. Organum rationis, sapphirus mentis.
  • A corgi and a capybara riding a turtle.

    Corgi, capybara, turtle.

  • A sapphire medallion with a corgi, a capybara, and a turtle.

    The sapphire.

  • A proof shield marked with the turnstile, carried on a turtle between a corgi and a capybara.

    The turnstile.

LogicArtificialis is a proposed European institute, in Bologna, for formalized mathematics and for a logic that is artificial in a precise sense: rules a machine can follow, syntax before interpretation. Its fields are formalized mathematics, computer-assisted proof, artificial logic, and mathematical logic.

Where a deposit here includes a Lean file, that file is what was uploaded to Zenodo. Modern Math is the collaborative shelf of the institute, not a second classification laid over the files.

Get in touch at logicartificialis.org or logicartificialis@gmail.com. Subscribe to the mailing list at logicartificialis@googlesites.com.

Open logicartificialis.org

distilledproof.org

Distilled Proof

From a draft to a signed proof.

Distilled Proof still: a corgi draws a sapphire drop onto a book marked with the turnstile, beside a capybara and a turtle.

Distilled Proof describes four movements. A draft is proposed, often in ordinary mathematical English and then in the syntax of a proof assistant. It is translated across systems. A kernel refuses what does not check. What survives is distilled: shorter, and signed.

The project is a companion of LogicArtificialis and of LogiBo, not a second institute, and not a mark on these records. Lean, Rocq, Isabelle, and Agda are instruments. The deposits stay on Zenodo.

Open distilledproof.org
Browse the catalog