Leanfying - Is It a Good Idea?

The first time that i teach real analysis with epslons and deltas, they are very confused. First, while we don't teach it right, we teach it as some abstract nonsense. Nay, how much precision do you want the answer to be? If you can always find a function, if you have to go out far enough in your sequence so that yu're within epselon of whatever result you want, that's all epselon and deltas are. But those are particularly amenable to leanfying,. To make a lean you make a lean programme, follow that lean programme and have it verify that your proof is correct. Then go and write...