Chart type Updated 2025-07-16
Chart Updated 2025-07-16
jq ignore missing attribute Updated 2025-07-16
echo '[{"a": 1, "b": 2}, {"b": 3}]' | jq '.[] | select(.a) | .a'1 Cerebras Updated 2025-07-19
They didn't care about MLperf as of 2019: www.zdnet.com/article/cerebras-did-not-spend-one-minute-working-on-mlperf-says-ceo/
- 2023: www.eetimes.com/cerebras-sells-100-million-ai-supercomputer-plans-8-more/ Cerebras Sells $100 Million AI Supercomputer, Plans Eight More
Scientific visualization Updated 2025-07-16
jq Updated 2025-07-16
Yet another awk-like domain-specific language to do things from the CLI in a ridiculously short humber of character? Oh yes.
Fabless semiconductor company Updated 2025-07-16
The Math Genome Project Updated 2025-07-16
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.
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/1137047842159079474Owner:So apparently there will be proof checking, but no dependencies between proofs, you still have to pull request everything back and face the pain.
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)
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.
Bibliography:
Web-based proof assistant Updated 2025-07-16
A more verbose description of this at: Section "Website front-end for a mathematical formal proof system".
Human loss of fur Updated 2025-07-16
Interbreeding between archaic and modern humans Updated 2025-07-16
Early human migrations Updated 2025-07-16
Early expansions of hominins out of Africa Updated 2025-07-16
Human evolution Updated 2025-07-16
The key cladograms:
- Hominoidea level for extant species separation
- Australopithecine level for extinct species separation: en.wikipedia.org/w/index.php?title=Homo&oldid=1155900663#Phylogeny
Australopithecine Updated 2025-07-16
Ape subclade Updated 2025-07-16
Ape Updated 2025-07-16
Simian subclade Updated 2025-07-16
Simian Updated 2025-07-16
Primate subclade Updated 2025-07-16
There are unlisted articles, also show them or only show them.
