TPIL4 PR reviews

Stream: general

[Timo Carlin-Burns]

There are many small PRs to Theorem Proving in Lean 4 languishing. Is there anybody with write access who might have time to take a look at the queue? Many of them are simple typo fixes or clarifications, and it's good to get clarifications in sooner than later. Recently I answered a question in new members that was the exact point of confusion that I opened a PR to clarify back in July.

[Yaël Dillies]

cc @Jeremy Avigad

[Jeremy Avigad]

I believe @David Thrane Christiansen is now in charge of maintaining the Lean documentation. David, how can I help?

[David Thrane Christiansen]

Thanks for bringing this up! How about I do a pass through the queue, and if there's anything I'm in doubt about, I'll ask you?

[Jeremy Avigad]

That would be great! Thanks.