Amniote by Ciro Santilli 40 Updated 2025-07-16
Name origin: amnion, a pellicle that covers embryos of both eggs and also during pregnancy.
Includes:
Does not include amphibians. If you include them, you have the tetrapods.
Appears to support multiple proof assistant backends including Lean, Hol and Coq.
A discussion on the Lean Zulip: leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20Math.20Genome.20Project/near/352639129. Lean people are not convinced about the model in general it seems however.
TODO not viewable without login?
Has conjectures feature.
Built by this dude John Mercer:He must be independently wealthy or something to do such a project? What a hero. But he seems to have jobs. On the side? Hardcore.
Ciro Santilli asked: discord.com/channels/1096393420408360989/1096393420408360996/1137047842159079474
Does the website actually automatically check the formal proofs, or is this intended to be implemented at some point? And if yes, is it intended to allow proofs to depend on other proofs of the website (possibly by other people)
Owner:
Hi Ciro, yes we will be releasing in-browser proof assistant environments/checkers (e.g. Lean). Our goal is not to replace the underlying open-source repos (e.g. Mathlib) so the main dependency will be on the current repos; then when statement formalizations and proofs come in and are certified they can be PR'd to the respective repos. So we will be the source of truth for the informal latex code but only a stepping stone and orchestration layer on the way to the respective formal libraries.
So apparently there will be proof checking, but no dependencies between proofs, you still have to pull request everything back and face the pain.
Famous conjecture by Ciro Santilli 40 Updated 2025-07-16
This section groups conjectures that are famous, solved or unsolved.
They are usually conjectures that have a strong intuitive reasoning, but took a very long time to prove, despite great efforts.
Physics by Ciro Santilli 40 Updated 2025-07-16
Physics (like all well done science) is the art of predicting the future by modelling the world with mathematics.
And predicting the future is the first step towards controlling it, i.e.: engineering.
Ciro Santilli doesn't know physics. He writes about it partly to start playing with some scientific content for: OurBigBook.com, partly because this stuff is just amazingly beautiful.
Ciro's main intellectual physics fetishes are to learn quantum electrodynamics (understanding the point of Lie groups being a subpart of that) and condensed matter physics.
Every science is Physics in disguise, but the number of objects in the real world is so large that we can't solve the real equations in practice.
Luckily, due to emergence, we can use uglier higher level approximations of the world to solve many problems, with the complex limits of applicability of those approximations.
Therefore, such higher level approximations are highly specialized, and given different names such as:
As of 2019, all known physics can be described by two theories:
Unifying those two into the theory of everything one of the major goals of modern physics.
Figure 1.
xkcd 435: Fields arranged by purity
. Source. Reductionism comes to mind.
They might have shut down, but they still have the cutest name! And they've made some cute inscriptions too, see: HHTT
Immune system by Ciro Santilli 40 Updated 2025-07-16
A cool thought: bacteria like E. Coli replicate every 20 minutes. A human replicates every 15 years. So how can multicellular beings possibly cope with the speed of evolution of parasites?
The answer is that within us, the adaptive immune system is a population of cells that evolves very quickly. So in a sense, within our bodies there is fast cell-level non-inheritable evolution happening daily!

Pinned article: Introduction to the OurBigBook Project

Welcome to the OurBigBook Project! Our goal is to create the perfect publishing platform for STEM subjects, and get university-level students to write the best free STEM tutorials ever.
Everyone is welcome to create an account and play with the site: ourbigbook.com/go/register. We belive that students themselves can write amazing tutorials, but teachers are welcome too. You can write about anything you want, it doesn't have to be STEM or even educational. Silly test content is very welcome and you won't be penalized in any way. Just keep it legal!
We have two killer features:
  1. topics: topics group articles by different users with the same title, e.g. here is the topic for the "Fundamental Theorem of Calculus" ourbigbook.com/go/topic/fundamental-theorem-of-calculus
    Articles of different users are sorted by upvote within each article page. This feature is a bit like:
    • a Wikipedia where each user can have their own version of each article
    • a Q&A website like Stack Overflow, where multiple people can give their views on a given topic, and the best ones are sorted by upvote. Except you don't need to wait for someone to ask first, and any topic goes, no matter how narrow or broad
    This feature makes it possible for readers to find better explanations of any topic created by other writers. And it allows writers to create an explanation in a place that readers might actually find it.
    Figure 1.
    Screenshot of the "Derivative" topic page
    . View it live at: ourbigbook.com/go/topic/derivative
  2. local editing: you can store all your personal knowledge base content locally in a plaintext markup format that can be edited locally and published either:
    This way you can be sure that even if OurBigBook.com were to go down one day (which we have no plans to do as it is quite cheap to host!), your content will still be perfectly readable as a static site.
    Figure 2.
    You can publish local OurBigBook lightweight markup files to either https://OurBigBook.com or as a static website
    .
    Figure 3.
    Visual Studio Code extension installation
    .
    Figure 4.
    Visual Studio Code extension tree navigation
    .
    Figure 5.
    Web editor
    . You can also edit articles on the Web editor without installing anything locally.
    Video 3.
    Edit locally and publish demo
    . Source. This shows editing OurBigBook Markup and publishing it using the Visual Studio Code extension.
    Video 4.
    OurBigBook Visual Studio Code extension editing and navigation demo
    . Source.
  3. https://raw.githubusercontent.com/ourbigbook/ourbigbook-media/master/feature/x/hilbert-space-arrow.png
  4. Infinitely deep tables of contents:
    Figure 6.
    Dynamic article tree with infinitely deep table of contents
    .
    Descendant pages can also show up as toplevel e.g.: ourbigbook.com/cirosantilli/chordate-subclade
All our software is open source and hosted at: github.com/ourbigbook/ourbigbook
Further documentation can be found at: docs.ourbigbook.com
Feel free to reach our to us for any help or suggestions: docs.ourbigbook.com/#contact