SJTULean/LeanFormalizer_SFT
Updated
•
2
None defined yet.
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.
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.
Jiaoyang
LuoTao
Xinze Wu
For collaboration inquiries or questions about our research, please feel free to reach out to us through:
© 2024 SJTU AI4MATH Lab - Lean4 Research Group. All Rights Reserved.