Zulip Chat Archive

Stream: maths

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: Dec 20 2023 at 11:08 UTC