Incoming links: Independently wealthy
It is a bit hard to decide if those people are serious or not. Sometimes it feels scammy, but sometimes it feels fun and right!
Particularly concerning is the fact that they are not a not-for-profit entity, and it is hard to understand how they might make money.
Charles Simon, the founder, is pretty focused in how natural neurons work vs artificial neural network models. He has some good explanations of that, and one major focus of the project is their semi open source spiking neuron simulator BrainSimII. While Ciro Santilli believes that there might be insight in that, he also has doubts if certain modules of the brain wouldn't be more suitable coded directly in regular programming languages with greater ease and performance.
FutureAI appears to be Charles' retirement for fun project, he is likely independently wealthy. Well done.
- www.aitimejournal.com/interview-with-charles-simon-ceo-and-founder-futureai
- 2022 raised 2 million USD:
Creativity and AGI by Charles Simon's at AGI-22 (2022)
Source. Sounds OK!- youtu.be/ivbGbSx0K8k?t=856 general structure of the human brain 86B total, matching number of neurons in the human brain, with:
- 14B: brainstem
- 16B: neocortex
- 56B: cerebelum
- www.youtube.com/watch?t=1433 some sequencing ideas/conjectures
Machine Learning Is Not Like Your Brain by Future AI (2022)
Source. Contains some BrainSimII demos.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 closed source? Really? www.themathgenome.com/pricing
TODO not viewable without login?
Has conjectures feature.
Built by this dude John Mercer: www.linkedin.com/in/johnmercer/. He must be independently wealthy or something? What a hero.
A failed Hacker News self post: news.ycombinator.com/item?id=35775071
Ciro Santilli asked: discord.com/channels/1096393420408360989/1096393420408360996/1137047842159079474Owner:So apparently there will be proof checking, but nodependencies between proofs, you still have to pull request everywhing 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.