Fixed version of mathlib4 used in annotation system
To use this project, clone it to your local first:
git clone https://github.com/frenzymath/lean-v4130-fixed.gitThen run lake update to update dependency.
Now you can test your answer (written in a .lean file in the same folder) to check if it is compatible with version 4.13.0.
The corresponding mathlib4 doc page address for this specific version is https://console.siflow.cn/siflow/draco/ai4math/wlli/doc-page-v1/