Zulip Chat Archive

Stream: general

Topic: What is worth a paper?


view this post on Zulip 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.

view this post on Zulip 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/

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Mar 22 2020 at 20:21):

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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Mar 22 2020 at 20:33):

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

view this post on Zulip Yury G. Kudryashov (Mar 24 2020 at 06:36):

#2228 Proof works, still needs polishing

view this post on Zulip Johan Commelin (Mar 24 2020 at 08:33):

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

view this post on Zulip Yury G. Kudryashov (Mar 24 2020 at 13:09):

Not in the first PR.

view this post on Zulip 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.

view this post on Zulip 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: May 14 2021 at 23:14 UTC