Second grade student

Stream: maths

[kali]

Good evening,

I am currently in high school and I have a lot of difficulty in mathematics.
I started competitve programming a few months ago to practice solving problems and learn programming.

3 days ago I discovered the proof wizards and I would like to know if it is adapted to a student of my level?

I am learning lean 3 with this guide: https://leanprover.github.io/theorem_proving_in_lean/index.html.

I would have liked to start doing geometry but the mathematics in the mathlib library is too complicated for me.
I have seen other libraries but it seems to be usable only for abstract geometry.

thanks

[Kevin Buzzard]

I've worked with high school kids in the UK and the main problem is that proof assistants like lean are focused on rigorous proofs of theorems, but the UK syllabus before university is mostly focused on calculations, so students have not really got much experience in what lean is good at. The natural number game works with schoolkids but right now the other obvious target, namely Euclidean geometry, is still rather difficult to do in lean, especially with no pictures

[kali]

That's exactly what I'm looking for.
As you say, I would like to do some calculus exercises in geometry and I can't figure out how to do it with lean.
Do you know a library for that?

[kali]

(deleted)