diff --git a/profile/README.md b/profile/README.md
index e083936..6436217 100644
--- a/profile/README.md
+++ b/profile/README.md
@@ -51,6 +51,7 @@
 | <img alt="む, mu, brushed in its three strokes, in pure Nix" src="https://raw.githubusercontent.com/piabrota/mu/960984b928062b5cf043001e072322df51f106fa/docs/drawings/mu.svg" width="64"/> | [**mu**](https://github.com/piabrota/mu) | The company chart: the dogma, the standards, the journal and the index of the org's repositories. | none | CC BY 4.0, AGPL-3.0, MPL-2.0 |
 | 道場 | [**dojo**](https://github.com/piabrota/dojo) | The umbrella of the piabrota projects. Being set up. | none yet | MPL-2.0 |
 | | [**ondecomer**](https://github.com/aracyla/onde-comer) | A site that lists the restaurants of Brazil, with filters for category, location and more. For now it covers only the city of Rio de Janeiro. | [https://aracyla.github.io/onde-comer/](https://aracyla.github.io/onde-comer/) | N/A |
+| <img alt="A neural network flowing into the universal quantifier, drawn from Desmos equations" src="https://raw.githubusercontent.com/h0ffmann/proof/361e50fb1cea81433d50c941db4f00363af2bd75/docs/logo/logo.svg" width="128"/> | [**proof**](https://github.com/h0ffmann/proof) | **Incubating.** Specifications written and proved in Lean 4, with Haskell and Rust implementations checked against them, and data experiments with papers. Formerly dogma. | none | MPL-2.0 |
 
 The drawings and the picture of the room load from each project's repository at a pinned commit;
 none is copied here. ihero, agents, dojo and ondecomer have no drawing yet.
diff --git a/profile/README.pt-BR.md b/profile/README.pt-BR.md
index 3c914f0..98e9013 100644
--- a/profile/README.pt-BR.md
+++ b/profile/README.pt-BR.md
@@ -52,6 +52,7 @@
 | <img alt="む, mu, brushed in its three strokes, in pure Nix" src="https://raw.githubusercontent.com/piabrota/mu/960984b928062b5cf043001e072322df51f106fa/docs/drawings/mu.svg" width="64"/> | [**mu**](https://github.com/piabrota/mu) | O chart da empresa: o dogma, os padrões, o diário e o índice dos repositórios da org. | nenhum | CC BY 4.0, AGPL-3.0, MPL-2.0 |
 | 道場 | [**dojo**](https://github.com/piabrota/dojo) | O umbrella dos projetos do piabrota. Em montagem. | ainda não | MPL-2.0 |
 | | [**ondecomer**](https://github.com/aracyla/onde-comer) | Um site que lista os restaurantes do Brasil, com filtros por categoria, localização e mais. Por enquanto, o site cobre só a cidade do Rio de Janeiro. | [https://aracyla.github.io/onde-comer/](https://aracyla.github.io/onde-comer/) | N/A |
+| <img alt="Uma rede neural que flui para o quantificador universal, desenhada com equações do Desmos" src="https://raw.githubusercontent.com/h0ffmann/proof/361e50fb1cea81433d50c941db4f00363af2bd75/docs/logo/logo.svg" width="128"/> | [**proof**](https://github.com/h0ffmann/proof) | **Em incubação.** Especificações escritas e provadas em Lean 4, com implementações em Haskell e Rust conferidas contra elas, e experimentos de dados com artigos. Antes se chamava dogma. | nenhum | MPL-2.0 |
 
 Os desenhos e a foto do quarto carregam do repositório de cada projeto, em um commit fixado.
 Nenhuma imagem é copiada para cá. ihero, agents, dojo e ondecomer ainda não têm desenho.