New Open Source Project: Infinity Archive - Lean4 Mathematic

Stream: general

[Xinze Li(Moqian)]

Hi everyone! I just released an open source project that I hope might be useful for the Lean community.

Infinity Archive is a browser-based mathematical IDE for Lean4. I'm still learning Lean myself (coming from a pure math background) and built this with AI assistance as both a learning project and hopefully something useful for others getting started with Lean.

:www: Live Demo: https://inftychi.vercel.app
:books: GitHub: https://github.com/Xinze-Li-Bryan/inftychi

What works now:

• Browser-based Lean4 environment (no local setup needed, though you need to create an account)
• Multi-file project support
• Integration with Mathlib theorems (searchable)
• Real-time verification (though can be slow on complex proofs)

Current limitations:

• Still rough around the edges and needs optimization
• Performance isn't great for large projects yet
• Requires account creation (wallet OR email)
• Built more for learning/experimenting than serious research

Future hopes:

• AI-assisted proof development
• Better performance and user experience
• Real-time collaboration features
• Maybe a true guest mode for just trying it out

I'm hoping that by open-sourcing it and getting feedback from people who actually use Lean, we can gradually make it more useful. Right now it's more like "lean4web with multi-file support" but with bigger ambitions.

Any feedback, suggestions, or contributions would be incredibly helpful as I continue learning both Lean and what the community actually needs!

Thanks for building such an amazing ecosystem! :folded_hands:

[Jireh Loreaux]

Xinze-Li(Moqian) said:

a zero-friction environment

except you need to link a digital wallet (?!?!)

[Xinze Li(Moqian)]

@Jireh Loreaux

Also worth noting - we're only on Sepolia testnet, so there's no financial risk or real ETH involved. It's just for testing the attribution features.

But you're right that "zero-friction" is misleading if you need any account at all. I should add a true guest/anonymous mode for just trying out the IDE.

Thanks for the UX feedback! :folded_hands:

[Jireh Loreaux]

For what it's worth, I don't even see a way to do email registration.

[Xinze Li(Moqian)]

@Jireh Loreaux You're absolutely right, and I apologize for the confusion! There's no email registration at all - I misspoke.

The actual design uses MetaMask wallet's public key directly for user identification (on Sepolia testnet, no real money involved). I thought this would be simpler than traditional email/password signup, but you're right that it's not "zero-friction" for people who don't have MetaMask.

Definitely need to add a proper guest mode for just trying the IDE. Thanks for the correction - I clearly need to be more careful about describing my own features! :sweat_smile: