hhu-adam / Robo

A game for learning lean 4 where a cute little Robo joins you on your exploration of the Mathiverse. The game is in German 🇩🇪

https://adam.math.hhu.de

Apache License 2.0

16 stars 9 forks source link

Babylon Level 4 Latex-summary mismatch #32

Closed bernborgess closed 3 months ago

bernborgess commented 3 months ago

In the 4th level of Babylon:

4_6_summe The formula states $$\sum{i=0}^{n}{(2n+1)} = n^2$$ Which is false for many examples. The statement in lean induces it to actually be $$\sum{i=0}^{n-1}{(2i+1)} = n ^2$$ I would change it myself and open a PR, but I couldn't find where it is defined in the repo.

TentativeConvert commented 3 months ago

Thank your for the report! I actually spotted the same typo a few days ago and corrected it in the repository:

https://github.com/hhu-adam/Robo/blob/fc1de96df4abc22c54b6b5c027f1886cda230972/Game/Levels/Sum/L04_SumOdd.lean#L20

I guess the fix will go live within the next week.