Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Two small gems in the AFP

Email Gateway (Aug 22 2022 at 16:32):

From: Lawrence Paulson <lp15@cam.ac.uk>
For your holiday enjoyment:

“A formalisation of Snyder’s simple and elegant proof of the Mason–Stothers theorem, which is the polynomial analogue of the famous abc Conjecture for integers.”

https://www.isa-afp.org/entries/Mason_Stothers.html

“An executable functional implementation of the Median-of-Medians algorithm for selecting the k-th smallest element of an unsorted list."

https://www.isa-afp.org/entries/Median_Of_Medians_Selection.html

Both thanks to Manuel Eberl.

Larry

Last updated: May 07 2024 at 01:07 UTC