Skip to content

Add h0ffmann/proof as an incubating project #12

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
h0ffmann merged 1 commit into from
Nov 9, 2026
Merged

Add h0ffmann/proof as an incubating project #12

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions profile/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
1 change: 1 addition & 0 deletions profile/README.pt-BR.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
Loading