There will be folders named Week-1, Week-2 etc. Click the current on the one you want to solve. (Week order will be messed up due to how GitHub decides precendence).
Each folder will have a readme will have a README.md with the two challenges for that week. One will be a theorem proving problem, and the other a programming related question. If you want to add your solution you must clone the repo, and submit a pr with your solution with a filename in the format of preferred-name.lean. Your file should have a comment at the top with your discord username and whether you are using Lean or Lean 4. (Lean may be better for some challenges because of mathlib).
Last notice. Your function names should start with the week and week number, along with _theorem if you are soving the theorem question or _programming if you are solving the programming oriented question. You can solve both if you want. Example function name: week4_theorem.
Using Lean 4's FFI is forbidden. (Worried people will use C for code optimization) Good Luck!