In Memoriam: Christopher Hoskin

Stream: general

[Patrick Massot]

Dear Lean community,

We, the Mathlib maintainer and reviewer teams, are saddened to learn of the passing of regular Mathlib contributor Christopher Hoskin. You can find his obituary in The Guardian.

Christopher contributed many commits to both mathlib3 and mathlib4. He was active in the community until his untimely death. We will endeavor to continue the work from his open pull requests.

[Yaël Dillies]

Although I have no idea when he started using Lean, I know for sure that Chris and I became mathlib contributors near simultaneously in mid-2021. Our formalisation interests were quite close: he was moving forward the order library for applications to functional analysis and I was honored to review his PRs on the various order topologies he needed. His GitHub page still proudly displays his mathlib achievements. I will remember Chris as a very kind person and prompt contributor, who had become valued for his expertise and social approach.

[Nick Adfor]

It is truly sorrowful to learn that the young Mathlib community has lost a member so prematurely.

Rest in peace.

"Blessed are the dead which die in the Lord from henceforth: Yea, saith the Spirit, that they may rest from their labours; and their works do follow them." (Revelation 14:13, KJV)

[Wrenna Robson]

May his memory be a blessing.

[Violeta Hernández]

I've taken the liberty of tagging all of his PRs with please-adopt, and I've taken one over at #33831. The least we can do for him is to minimize his unfinished business.

[Filippo A. E. Nuccio]

Violeta Hernández said:

I've taken the liberty of tagging all of his PRs with please-adopt, and I've taken one over at #33831. The least we can do for him is to minimize his unfinished business.

Some of them had already been adopted. Have you double-checked before?

[Violeta Hernández]

Sorry, I didn't notice any of them being already adopted.