Nature news story

Stream: condensed mathematics

[Johan Commelin]

https://www.nature.com/articles/d41586-021-01627-2

[Johan Commelin]

Peter Woit has already updated his blogpost to mention the Nature story: https://www.math.columbia.edu/~woit/wordpress/?p=12364

[Johan Commelin]

https://news.ycombinator.com/item?id=27559917

[Adam Topaz]

One of the comments mentions: "....Lean's core is not completely sound" :scared:

[Anatole Dedecker]

Adam Topaz said:

One of the comments mentions: "....Lean's core is not completely sound" :scared:

Mentioning that famous discussion about quotients... :tired:
Should there be a doc page about that quotient """issue""" that could be linked in these kind of situations ?

[Oliver Nash]

What’s the difference between completely sound and sound? Is false, slightly true?

[Johan Commelin]

If a system is sound, you may have an infinite sequence of proofs converging to a proof of false. If a system is completely sound, that cannot happen.
/s /jk /troll

[Adam Topaz]

Who is this HN user deadbeef57? :wink: (not me, but please don't dox yourself)

[Johan Commelin]

/me has no clue :oops: :crazy: /s

[Johan Commelin]

Just doxed myself on HN

[Adam Topaz]

Johan, now everyone will be able to find your private GPG key... https://math.commelin.net/files/precious.jpg

[David Michael Roberts]

Scholze and Clausen say they have already found simpler, ‘condensed’ proofs of a number of profound geometry facts, and that they can now prove theorems that were previously unknown. They have not yet made these public.

I guess this is referring to the stuff about https://en.wikipedia.org/wiki/Coherent_sheaf_cohomology#Finite-dimensionality, from memory in the Masterclass lectures? Or the musings about Hodge theory from the Zoom party, that Johan mentioned briefly on HN? Or something else to look forward to...

[David Michael Roberts]

I should say, I mean the "simpler, 'condensed' proofs". The "previously unknown" theorems of course I would have, by definition, no idea about!

[Kevin Buzzard]

Finiteness of sheaf cohomology is mentioned in analytic.pdf as an application of this stuff

[David Michael Roberts]

Thanks, I didn't go back and check. I guess the quote I gave is an example of ambiguous writing. What exactly "these" in the last sentence refers to is ambiguous, and false if one takes is to mean all the proofs mentined in the previous sentence.

[David Michael Roberts]

I guess what I mean to ask is: is it ok to mention in print that there are potential applications to Hodge theory?

[Kevin Buzzard]

I guess the Nature guy spoke to both Dustin and Peter so probably it's best that you do too

[Johan Commelin]

@David Michael Roberts I agree with Kevin that it's best to talk to Dustin and Peter directly. But if you want a "simple" condensed proof of an old complicated result, then the final part of Condensed.pdf contains a proof of coherent duality for schemes.

[Johan Commelin]

The other applications mentioned in the masterclass are not yet written down in detail, as far as I know

[David Michael Roberts]

Ok, thanks, both. I just wanted to do the most obvious check first.

[Riccardo Brasca]

Thank's to Nature's article, I've been contacted by an Italian scientific journalist to speak in a pop science radio program about LTE. This will be of very limited interested unless you speak Italian (and even in that case I don't think I will speak more than a couple of minutes). I have no idea why they contacted me instead of Damiano or Filippo. In any case I find it amazing that journalists are interested in Lean!

[Yaël Dillies]

This little octopus smiley depicts us slowly taking over the world, right? :octopus: :octopus:

[Peter Scholze]

Jordan Ellenberg chimes in: https://bigthink.com/technology-innovation/artificial-intelligence-replace-mathematicians

[Kevin Buzzard]

That's great news Riccardo!

[Scott Morrison]

I like Jordan's article a lot!

[David Michael Roberts]

I don't want to cast aspersions, but "Proof assistance" looks like an over-zealous editor read "Proof assistants" and felt like correcting it (particularly poor, when the headline before explicitly mentioned "assistant"!)

[David Michael Roberts]

But that's just my picky editor side. It's great the news is spreading!