Much of this section will be dumped at Section "Website front-end for a mathematical formal proof system" instead.
If Ciro Santilli ever becomes rich, he's going to solve this with: website front-end for a mathematical formal proof system, promise.
The website was dead as of February 2025. Last archive: web.archive.org/web/20240418004442/http://www.themathgenome.com/ Pings:They were seeking help on May 2024:so its likely the followup death. LinkedIn post gives basic stack: MERN stack, Heroku, Supabase/MongoDB Atlas.
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.
Source code:
Their 2025 current installation method is bullshit, recommends VS Code extension on Ubuntu. Lol.
From CLI:
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
source $HOME/.elan/env
Then when you run:
lean
it downloads the lean executable for you. Insane shit, could only come from a Microsoft mindset.
This tutorial has the merit of actually trying you to do some meaningful mathematics before teaching you a billion items of syntax and dependent type theory nuances.
This used to have the best name ever allowing you to say:to English speakers and watch their faces drop.
But in 2023 the bastards renamed it to "Rocq", presumably pronounced "rock". Why, God, why.
This will never work but OK. New custom language after Lean.
It seems to implement Zermelo-Fraenkel set theory.

Articles by others on the same topic (0)

There are currently no matching articles.