Zulip Chat Archive

Stream: general

Topic: What is worth a paper?

Yury G. Kudryashov (Mar 22 2020 at 19:17):

While I understand what is worth writing a paper in pure mathematics, I have no idea what mathlib-related activities might be worth a paper, what journals would accept such paper, and which of those journals are good/bad.

Patrick Massot (Mar 22 2020 at 19:29):

You can have a look at the list of papers at https://leanprover-community.github.io/links/

Patrick Massot (Mar 22 2020 at 19:30):

The most relevant to you are the papers about Hensel lemma, Cap set problem, Continuum hypothesis, perfectoid spaces.

Yury G. Kudryashov (Mar 22 2020 at 19:56):

If I look at my own contributions, then may be the most significant ones are in analysis: MVT, Gronwall's inequality and uniqueness of solutions of an ODE, Darboux theorem.
May be we should write a paper about the current status of analysis/calculus in Lean, including derivatives, manifolds, and integrals.
This would be one more reason to have #1944 finalized & merged.

Patrick Massot (Mar 22 2020 at 20:18):

The issue is that only manifolds are a new formalization target. Publishing about stuff that was already formalized in some other proof assistant is trickier. You would need a convincing story about how things were different (and better) in your case.

Patrick Massot (Mar 22 2020 at 20:19):

Talking about ODEs, what is the status of the inverse function theorem? You started something, but was it ever finished?

Patrick Massot (Mar 22 2020 at 20:21):

Analysis is difficult for publications because Isabelle already has a huge analysis library.

Simon Hudon (Mar 22 2020 at 20:22):

Btw @Patrick Massot the publication page is mission Leo and Sebastian's macro paper and my pointer optimization paper

Patrick Massot (Mar 22 2020 at 20:22):

Sébastien can probably tell us whether you and him already did some stuff beyond what is in Isabelle (apart from the manifold folder, but Sébastien seems to be tired of pushing that bit, or maybe he wants analytical manifolds).

Patrick Massot (Mar 22 2020 at 20:23):

I'm not maintaining that list, but I'm sure Rob is open to PR to this page.

Yury G. Kudryashov (Mar 22 2020 at 20:33):

I'll try to PR the inverse function theorem today or tomorrow.

Yury G. Kudryashov (Mar 24 2020 at 06:36):

#2228 Proof works, still needs polishing

Johan Commelin (Mar 24 2020 at 08:33):

@Yury G. Kudryashov Will there also be a version for manifolds?

Yury G. Kudryashov (Mar 24 2020 at 13:09):

Not in the first PR.

Patrick Massot (Mar 24 2020 at 13:10):

We don't have submanifolds yet. Last time I asked Sébastien he no precise plans for submanifolds in mathlib.

Patrick Massot (Mar 24 2020 at 13:25):

Simon Hudon said:

Btw the publication page is mission Leo and Sebastian's macro paper and my pointer optimization paper

https://github.com/leanprover-community/leanprover-community.github.io/pull/6

Last updated: Dec 20 2023 at 11:08 UTC