Challenge 5

Stream: general

[Wojtek Wawrów]

Hi, I've been trying challenges from this page https://github.com/kbuzzard/xena/blob/master/Maths_Challenges/README.md and I was unable to finish challenge 5, so I decided to check out the solution, but it appears that Lean doesn't recognize that solution as valid: it complains that that the two expressions are not definitionally equal. How should this one be solved then? I'm having trouble transforming d.succ into d+1.

[Yakov Pechersky]

docs#nat.succ_eq_add_one

[Eric Rodriguez]

d.succ is definitionally equal to d+1, if I look at the solution the real issue is that some of the items aren't in the correct order

[Eric Rodriguez]

you should change the change so that things are in the exact order as before

[Wojtek Wawrów]

Huh ok, I see

[Wojtek Wawrów]

It also seems challenge 8 is completely broken...

[Kyle Miller]

@Wojtek Wawrów finset.sum_range_succ was renamed to finset.sum_range_succ_comm five months ago, and finset.sum_range_succ got a new meaning.

[Kyle Miller]

For challenge 8's solution, add import algebra.group.basic to the top.

[Kyle Miller]

This phenomenon is known as "bit rot" -- code seems to slowly decay over time. It happens particularly quickly for code that uses but isn't part of mathlib.

[Kevin Buzzard]

Thanks! I can try and update the challenges

[Patrick Massot]

The solution is known, you can put them in a proper Lean project on GitHub if they aren't already and setup to update bot, as explained at https://leanprover-community.github.io/ci.html

[Kevin Buzzard]

Heh, I wrote those challenges a very long time ago :-) The solution is known now...