metadata

title: README
emoji: 🐨
colorFrom: blue
colorTo: indigo
sdk: static
pinned: false

SJTU AI4MATH Lab - Lean4 Research Group

About Us

We are a research group focused on Lean4 formalization at Shanghai Jiao Tong University (SJTU), jointly operated by Jiao Ying Technology and the SJTU AI4MATH Laboratory. Our primary research direction involves translating natural language into Lean4 formal proofs.

Research Focus

Natural Language to Lean4 translation
Formal mathematics verification
Dataset creation and curation for Lean4
AI-assisted formal proof development

Maintained Projects

Our group maintains various datasets and models specifically designed for Lean4 formalization. These resources aim to bridge the gap between natural language mathematical expressions and formal Lean4 proofs.

Team Members

Jiaoyang
- Email: [email protected] | [email protected]
- GitHub: InuyashaYang
LuoTao
- Email: [email protected]
Xinze Wu
- Email: [email protected]
- GitHub: XinzeWu

Contact

For collaboration inquiries or questions about our research, please feel free to reach out to us through:

Email: [email protected]
GitHub: Organization Repository

Affiliation

Jiao Ying Technology
AI4MATH Laboratory