Zulip Chat Archive
Stream: new members
Topic: mathlib merge master
AM (Jul 11 2022 at 18:37):
Hello, I'm a new user and I don't think I have permission to merge master in GitHub, can someone please help? Thanks!
Johan Commelin (Jul 11 2022 at 19:06):
@AM Hi! What exactly do you mean with merging master? Do you want push access for non-master branches? Can you also explain a bit what kind of project you are (planning) to work on?
AM (Jul 12 2022 at 16:52):
Yes, I'd like push access for non-master branches. I'm currently working on a proof of Descartes' circle theorem for an REU I'm participating in. Thanks!
Kevin Buzzard (Jul 12 2022 at 18:59):
You'll need to post your github userid I guess ;-)
Kevin Buzzard (Jul 12 2022 at 19:01):
Who are you doing the REU with? I think it's great to see some geometry like this in Lean. I would like to see a geometry IMO problem formalised in Lean, just to prove that we can do this sort of thing nowadays.
Bolton Bailey (Jul 12 2022 at 19:07):
With the recently announced polyrith tactic, I would be interested to see if the Descartes theorem can be proved using that.
Archana M (Jul 12 2022 at 19:28):
My github userid is AAM246. I'm working with Professor Alex Kontorovich at Rutgers University!
Archana M (Jul 12 2022 at 19:30):
I had heard about the polyrith tactic but didn't realize it was fully developed yet. Do you know where I can find more information on this?
Bolton Bailey (Jul 12 2022 at 19:37):
Archana M said:
I had heard about the polyrith tactic but didn't realize it was fully developed yet. Do you know where I can find more information on this?
Kevin Buzzard (Jul 12 2022 at 22:06):
Or the tutorial Heather just posted!
Joseph Myers (Jul 17 2022 at 14:35):
Kevin Buzzard said:
Who are you doing the REU with? I think it's great to see some geometry like this in Lean. I would like to see a geometry IMO problem formalised in Lean, just to prove that we can do this sort of thing nowadays.
Almost all recent IMO geometry problems can't yet be stated in an idiomatic way because of missing definitions (and associated API for those definitions) in mathlib. Most often betweenness / convexity and similar conditions (which might sometimes not actually be needed for the result to be true, but are included so contestants are less likely to need to deal with configuration-dependence), including variations such as referring to a particular arc of a circle, but also e.g. incenters, tangency, areas (i.e. linking geometry to the measure theory library, together with convexity).
As I mentioned to @David Wärn at IMO 2022, I'd like to get all six IMO 2019 problems into the mathlib archive, with problem 2 as an intermediate geometry goal, and what I have in mind for the convexity issues is to add definitions such as affine_segment in the affine space case and use those to build up the required definitions for betweenness, and then a future convexity / affine space refactor could replace such a definition by a more general segment for abstract affine combination spaces that works in both the semimodule and add_torsor contexts.
If you want an IMO geometry problem that doesn't run into such missing mathlib API and so might be done without a large number of preparatory PRs adding API, IMO 2008 problem 1 seems to be the most recent such problem.
Yaël Dillies (Jul 17 2022 at 14:37):
I am still thinking about the convexity refactor btw. This would solve your affine_segment problem.
Last updated: Dec 20 2023 at 11:08 UTC