[Om] OpenMath seminar Friday 3 November: Complex complex domains and self-documentation of formal mathematical properties

[Lars Hellström]

Not having heard anything to the contrary, I created a one-off zoom meeting for next week's seminar:
https://mdu-se.zoom.us/j/68335877011
(Long invitation below, if anyone needs that.)

Now for the scientific part:

Title:   Complex complex domains and self-documentation of formal mathematical properties

Speaker:   Lars Hellström

Time:  15:00 CET, Friday 3 November 2023.
(For those in other timezones, that's second 1699020000 in the Unix epoch, or Fri Nov 03 10:00:00 EDT 2023 in New York.)

ABSTRACT:

Many (maybe even most) elementary and special functions extend to accepting complex numbers as arguments, but these extensions are not always canonical; computer algebra systems tend to implement these functions so that they have branch cuts (discontinuities) in not always easily anticipated places, leading to surprising special cases in basic identities and also interoperability problems when different systems make different decisions on how to cut. The problem is known and also dealt with in the literature, but solutions tend to be messy. From the perspective of "high mathematics", a more unified approach would be to use Riemann surfaces — sets where each point corresponds to a complex number, but several different points may correspond to the same complex number, allowing all possible values for a function to be realised at some point of the Riemann surface, while preserving strict continuity of the function. Specific function branches may then be viewed as restrictions of the full function, and different choices may be reasoned about in that setting.

OpenMath does nothing to prevent taking Riemann surfaces as the domains of functions, but it does not provide much help with it either. In particular, the functions specialist who would like to take this route would be confronted by the very basic problem of how to formally specify that Riemann surface in the first place; there are no obvious tools for this within the official content dictionaries. That is however something that can be fixed at any time, by providing a new content dictionary with appropriate symbols, so even though complex analysis is not exactly my cup of tea, I though it an interesting exercise to formalise Riemann surfaces as a generic utility. Since there (to my knowledge) had not been any previous formalisation of comparable complexity and not chiefly expressing familiar algebraic identities, this also provides a stress test of the content dictionary format. What became apparent is that it is not sufficient to merely state formulae when they grow large, one must also provide clues to the human reader on what is going on, much as programmers do with comments within subroutines.

In this talk I will go through my Riemann-surface content dictionary to show how Riemann surfaces can be effectively formalised in a computer mathematics context, taking care to review the mathematical background (as I do not expect all listeners to be intimately familiar with these parts of mathematics) and show how compactly even some less trivial surfaces (such as that of the Lambert W function) may be specified. I will also introduce the comment1 content dictionary and discuss how its facilities could be used to make FMPs such as that of the Riemann-surface CD more comprehensible. Furthermore I will demonstrate some corresponding new features in my LaTeX package for writing OpenMath CDs.

END ABSTRACT.




ZOOM INVITATION:

Topic: OpenMath seminar
Time: Nov 3, 2023 15:00 Stockholm

Join Zoom Meeting
https://mdu-se.zoom.us/j/68335877011

One tap mobile
+46850539728,,68335877011# Sweden
+46844682488,,68335877011# Sweden

Dial by your location
        +46 850 539 728 Sweden
        +46 8 4468 2488 Sweden
        +46 8 5016 3827 Sweden
        +46 8 5050 0828 Sweden
        +46 8 5050 0829 Sweden
        +46 8 5052 0017 Sweden
Meeting ID: 683 3587 7011
Find your local number: https://mdu-se.zoom.us/u/ccqkwOhRNq

Join by SIP
68335877011 at 109.105.112.236
68335877011 at 109.105.112.235

Join by H.323
109.105.112.236
109.105.112.235
Meeting ID: 683 3587 7011

Join by Skype for Business
https://mdu-se.zoom.us/skype/68335877011