Infinity Archive

Stream: general

[Joachim Breitner]

Moqian schrieb:

:books: GitHub: https://github.com/Xinze-Li-Bryan/inftychi

This is a 404 (now)

[Yaël Dillies]

I think the website migrated to https://infinity-archive-blog.vercel.app/

[Eric Wieser]

How does this compare to gitpod or GitHub code spaces?

[Xinze Li(Moqian)]

Hi everyone, thanks for checking out the project!

About the GitHub repo: After the initial open source release, I got very little engagement or feedback, so I decided to close the repo temporarily to focus on improving the core features. I figured it's better to build something actually useful first before asking for community contributions.

Current status: This is still very much a prototype/proof-of-concept. Not production-ready, but the core functionality works.

Recent progress:

• Fixed multi-file imports - you can now properly use import Module.Name across files
• Added AI assistant for proof guidance (BYO API key - supports OpenAI/Claude/Gemini)
• Performance improvements - initial load down from 13+ seconds to 3-5 seconds
• Support for mixing LaTeX documentation with Lean proofs in the same workflow

Live prototype at: https://inftychi.vercel.app

@Eric Compared to Gitpod/Codespaces - this isn't a general-purpose IDE. It's more like Overleaf but for formal mathematics - specialized infrastructure for mathematical research with Lean. The focus is on:

• Seamlessly mixing informal mathematical writing (LaTeX) with formal proofs (Lean)
• AI-assisted proof development tailored for mathematics
• Research-oriented workflow rather than software development

Looking for collaborators: Since this is still in prototype stage, it's the perfect time to shape its direction. If anyone's interested in:

• Building better infrastructure for formal mathematics research
• Improving AI integration for proof assistance
• Or has ideas about what mathematicians actually need from such tools

Please reach out! Happy to re-open the repo for serious contributors.

Email: xbryanli.li@mail.utoronto.ca

[Xinze Li(Moqian)]

here is the screenshot of the current IDE:
image.png

[Notification Bot]

5 messages were moved here from #general > New Open Source Project: Infinity Archive - Lean4 Mathematic by Moqian.

[Eric Wieser]

I think you would have got a lot more interest if you started with a screenshot before!

[Xinze Li(Moqian)]

https://arxiv.org/html/2509.08267v1
Just find an interesting work
Exploring Formal Math on the Blockchain: An Explorer for Proofgold

[Xinze Li(Moqian)]

Haha right right, the picture seems more attractive than text

[Xinze Li(Moqian)]

@Eric Wieser Haha right right, the picture seems more attractive than text

[Xinze Li(Moqian)]

Here is our official website, https://inftychi-website.zeabur.app/.
Recently I find some engineers that helps me build the IDE+blockchain ecosystem. Hopefully they can let us enjoy a better lean developing environments soon. Here is the demo, it supports email sign in: https://inftychi.zeabur.app/

[Xinze Li(Moqian)]

e7719e45868368c7b971af0416af651a.png
e54ba0cfc28a661de0e8e0c44e17087b.png
da70eb2c03e0d5026a81440159610608.png
6dd65b8f71999a51156df989441e3483.png
5cac49ae1df99792bed170de8b1239d6.png
4fdf0c3703519b688cd40555e2b1b608.png

[Xinze Li(Moqian)]

Here are a few more pictures

[Xinze Li(Moqian)]

Also we just start a discord channels, still nobody here now hahah: https://discord.gg/HJrpetUw

[Xinze Li(Moqian)]

Recently we got more supports!