Topic: Algebraic closure Roadmap
Chris Hughes (Jan 12 2020 at 21:53):
I have written a new algebraic closure roadmap that covers the refactoring that needs to be done before algebraic closure is merged
Kevin Buzzard (Jan 12 2020 at 22:27):
What do you think about putting it in mathlib in the wiki pages? https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Future.20projects.20as.20Wiki.3F
Reid Barton (Jan 13 2020 at 00:09):
I will have more to say about your general question in the other topic later, but this kind of planned refactoring is best as an issue on Github, I think.
Rob Lewis (Apr 20 2020 at 11:22):
FYI, this paper just popped up for me on Google Scholar: Algebraically Closed Fields in Isabelle/HOL. It cites @Chris Hughes 's roadmap and @Kevin Buzzard.
Chris Hughes (Apr 20 2020 at 11:24):
That's actually @Kenny Lau 's roadmap
Rob Lewis (Apr 20 2020 at 11:27):
Oh, oops, sorry Kenny!
Last updated: May 12 2021 at 06:14 UTC