Scientific credibility
Formal proofs in Lean 4 (the classical Hopfield network) as a sign of engineering maturity, not a marketing claim.
Neural core · Research
MagicBrain Research
A research neural layer: spiking networks, local learning and a network architecture specified by a compact genome rather than designed by hand. Our own line of research, not a product: the code is open (PyPI 0.8.0) and is not used in products yet.
The problem
The ecosystem needs its own long-term R&D moat: a line of research into bio-inspired networks, not a wrapper around other people’s APIs. This is research, not a product, and its status is honestly recorded as Research.
Why existing solutions fail
Wrappers around other people’s models give you no scientific base of your own, and statically designed networks do not study how structure can form by itself. This is an open research question, not a solved problem — so we talk about observable properties and engineering maturity, with no claims of superiority over existing approaches.
How it works
We show engineering maturity, not a scientific result: formal proofs in Lean 4 for the classical Hopfield network (energy does not increase, ΔE≤0) and the observable behaviour of Hopfield recall. These proofs do not cover the TextBrain spiking network. There are no claims about speed-up or text-generation quality: on the evaluation bench the spiking network does not yet beat a bigram model.
Demo
Researchscreenshot
Technology
- Python
- Lean 4
- NumPy
Use cases
The ecosystem’s R&D moat
A long-term line of research and a scientific moat — not sold as a product.
Evidence
Lean 4: 21 statements about the classical Hopfield network, 0 sorry
It is proved that the energy of the classical Hopfield network does not increase (ΔE≤0). This is a re-formalisation of a classical result: the proofs do not cover the TextBrain spiking network. We show that the proofs build.
Reproduce: lake build
Hopfield recall: store a pattern → corrupt bits → recover it
Observable pattern-completion behaviour on corrupted input — behaviour only, with no scientific claims about effectiveness.
Reproduce: pytest -k pattern_memory
Cost the effect on your own figures
AVA is a process-economics calculator. In a couple of minutes it shows whether this pays off in your case — before any call, with no commitment.
Estimate with AVALet us look at your task
Tell us what needs solving. If it cannot be solved or will not pay off, we will say so up front, before any work starts.
or write to us directly: hello@xteam.pro