5 ms·

I think that right now it is not clear why condensed/liquid mathematics would be useful for PDEs. On the other hand, your question > Or does it "contain" topol

I think that right now it is not clear why condensed/liquid mathematics would be useful for PDEs. On the other hand, your question > Or does it "contain" topology in some sense, allowing people to continue working with notions of convergence obtained from norms? has a positive answer. You can, if you want, swap out topological spaces, and use condensed sets instead, and just continue with life as usual. At the same time, all of this is in fast paced development, so hopefully we will see some killer apps in the near future. But I expect them more in the direction of Hodge theory and complex analytic geometry.

wolverine876 5y ago
Thanks for sharing your expertise. Would you be open to sharing your background? Obviously it's not required, but it would help contextualize what you're saying for the interested non-mathematician; otherwise we're kinda stuck with 'some guy on the Internet said ...' syndrome. :)
- deadbeef57 5y ago
  Sure, I just created an account a couple of days ago, and my favourite username was already taken :oops: I'm Johan Commelin, https://math.commelin.net/ https://math.commelin.net/
  - wolverine876 5y ago
    Thank you! And welcome! Make yourself at home.
  - alimw 5y ago
    Hi! Imagine for a moment that your next project required you to develop a lot of functional analysis and PDE theory in Lean. Would you be tempted to build that on top of what you've done (or will have done) with condensed sets?
    - deadbeef57 5y ago
      Right now, I think I would go for that classical approach, simply because there is more supporting material for that in the library, and there are more people who understand that approach and can help contributing. (I'm talking specifically about functional analysis and PDEs here.) On the other hand, it should be a lot of fun to see if we can formalize the new proof by Clausen--Scholze of Serre duality. Using their machinery, the proof should simplify a lot. But this requires building complex analytic manifolds on top of condensed mathematics. So we would first need to set up those foundations.
  - rakhodorkovsky 5y ago
    clicked on the private key link; haven't laughed this much in days

wolverine876 5y ago

Thanks for sharing your expertise. Would you be open to sharing your background? Obviously it's not required, but it would help contextualize what you're saying for the interested non-mathematician; otherwise we're kinda stuck with 'some guy on the Internet said ...' syndrome. :)

deadbeef57 5y ago
Sure, I just created an account a couple of days ago, and my favourite username was already taken :oops: I'm Johan Commelin, https://math.commelin.net/ https://math.commelin.net/
- wolverine876 5y ago
  Thank you! And welcome! Make yourself at home.
- alimw 5y ago
  Hi! Imagine for a moment that your next project required you to develop a lot of functional analysis and PDE theory in Lean. Would you be tempted to build that on top of what you've done (or will have done) with condensed sets?
  - deadbeef57 5y ago
    Right now, I think I would go for that classical approach, simply because there is more supporting material for that in the library, and there are more people who understand that approach and can help contributing. (I'm talking specifically about functional analysis and PDEs here.) On the other hand, it should be a lot of fun to see if we can formalize the new proof by Clausen--Scholze of Serre duality. Using their machinery, the proof should simplify a lot. But this requires building complex analytic manifolds on top of condensed mathematics. So we would first need to set up those foundations.
- rakhodorkovsky 5y ago
  clicked on the private key link; haven't laughed this much in days