File size: 1,659 Bytes
b3c51e2 37f997a 2d6b4dd 1763ed9 2d6b4dd 37f997a |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 |
---
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]](mailto:[email protected]) | [[email protected]](mailto:[email protected])
- GitHub: [InuyashaYang](https://github.com/InuyashaYang)
- **LuoTao**
- Email: [[email protected]](mailto:[email protected])
- **Xinze Wu**
- Email: [[email protected]](mailto:[email protected])
- GitHub: [XinzeWu](https://github.com/XinzeWu)
## Contact
For collaboration inquiries or questions about our research, please feel free to reach out to us through:
- Email: [[email protected]](mailto:[email protected])
- GitHub: [Organization Repository](https://github.com/InuyashaYang)
## Affiliation
- Jiao Ying Technology
- AI4MATH Laboratory
---
© 2024 SJTU AI4MATH Lab - Lean4 Research Group. All Rights Reserved.
|