Hi @RickySkywalker 🤗
Niels here from the open-source team at Hugging Face. I discovered your work through Hugging Face's daily papers as yours got featured: https://huggingface.co/papers/2606.06523.
The paper page lets people discuss about your paper and lets them find artifacts about it (your code, library or demo for instance), you can also claim
the paper as yours which will show up on your public profile at HF, add Github and project page URLs.
I saw in your GitHub README that "The Lean repository and experiment codes will be available soon." That's fantastic news!
It'd be great to make your Lean4Agent framework, its FormalAgentLib library, and the experiment codes available on the 🤗 hub, to improve their discoverability/visibility.
We can add tags so that people find them when filtering repositories and link them to the paper page.
Uploading Code/Library
You can share your code directly on the Hugging Face Hub by creating a repository. This could include your Lean4 library (FormalAgentLib) and experiment codes. See here for a guide on creating repositories: https://huggingface.co/docs/hub/repositories-getting-started. You can push your Lean4 code and FormalAgentLib, and people can clone and use it directly.
After uploaded, we can also link the repositories to the paper page (read here) so people can discover your work.
You could also potentially build a demo for your framework on Spaces to showcase its formal modeling and verification capabilities, and we can provide you a ZeroGPU grant, which gives you A100 GPUs for free.
Let me know if you're interested/need any help regarding this!
Cheers,
Niels
ML Engineer @ HF 🤗
Hi @RickySkywalker 🤗
Niels here from the open-source team at Hugging Face. I discovered your work through Hugging Face's daily papers as yours got featured: https://huggingface.co/papers/2606.06523.
The paper page lets people discuss about your paper and lets them find artifacts about it (your code, library or demo for instance), you can also claim
the paper as yours which will show up on your public profile at HF, add Github and project page URLs.
I saw in your GitHub README that "The Lean repository and experiment codes will be available soon." That's fantastic news!
It'd be great to make your Lean4Agent framework, its FormalAgentLib library, and the experiment codes available on the 🤗 hub, to improve their discoverability/visibility.
We can add tags so that people find them when filtering repositories and link them to the paper page.
Uploading Code/Library
You can share your code directly on the Hugging Face Hub by creating a repository. This could include your Lean4 library (
FormalAgentLib) and experiment codes. See here for a guide on creating repositories: https://huggingface.co/docs/hub/repositories-getting-started. You can push your Lean4 code and FormalAgentLib, and people can clone and use it directly.After uploaded, we can also link the repositories to the paper page (read here) so people can discover your work.
You could also potentially build a demo for your framework on Spaces to showcase its formal modeling and verification capabilities, and we can provide you a ZeroGPU grant, which gives you A100 GPUs for free.
Let me know if you're interested/need any help regarding this!
Cheers,
Niels
ML Engineer @ HF 🤗