Bruce, please.

Yes. So I'm Bruce Miller, I work at the NISD in the United States.

We developed a program, LatechML, for converting latech to XML and other things for the purpose of the Digital Library of Mathematical Functions project, dllmf.nis.gov.

A big resource on special functions.

It led to a lot of interest in the mapping of latech to MathML to content to semantics and notations, etc, etc.

And the big project of well let's apply it to archive and been working with Dan and Michael over a number of years on these things.

And yeah, so there.

We may have been making some progress with archive, by the way.

So I just I'm a now PhD student of Michael's I think I just finished my master's thesis a week ago. So far, I've been my master's thesis working on translating small subsets of natural language logic and now I want to expand that to applying to mathematics on a corpus level, which means that I have probably very incomplete formalizations and I'm just starting to plan that.

Dennis.

So hi I'm Dennis from the University of Hamburg where I'm writing my PhD in the philosophy department and Peter Koepke and Bernhard Schröder brought me via the NaProsh project into formal mathematics and I'm currently still working with Bernhard Schröder on frame, a frame approach to

mathematical language and he will probably tell later sentence more about this.

Dennis, Dejan.

I'm happy to give my full introduction in the talk, but yeah, hi, I'm archives data shepherd when it comes to math syntax.

I'll leave it at that for now.

Okay, Bernhard.

Yeah, my name, my name is Bernhard Schröder from the University of Duisburg-Esten in Germany.

Yeah, I've been working with the language and linguist and I've been working with the language of mathematics for more than 15 years now.

And I'm currently working on the application of the frame theory to mathematical proofs.

I'm, as Dennis mentioned, working on the application of the frame theory to mathematical proofs and we look at proofs and see how gaps and proofs, implicit information is filled in, maybe with the help of frames that at least our assumption.

And we are looking with text linguistic methods towards proofs.

Thank you. Takuto.

Hello, this is Takuto Asakura, PhD candidate at University of Tokyo, and also a member of TechLive team.

I belong to a research group for natural language processing, and I'm interested in the small structures in formula and documents. So I'm currently doing kind of grounding, which is the task to associate meanings of each identifiers and other tokens in formula

to its meanings. I will give some talks in a few couple after seminar in this opportunity.

Thank you, Peter.

Right.

I'm a mathematician, mathematical logician and a set theorist, but over let's say 20 years have developed a strong interest in formal mathematics. And this has led together with Bernhard to the NAPOS project and program, and this means, I should perhaps spell out natural proof checking or natural

language proof checking. So, we want to do formal mathematics, starting from a rather natural controlled language. And I think we are making good progress, especially since a couple of years now because we have integrated the SAD project, very interesting old project into ours.

And we are now working to get the language even smoother and more efficient and so on. So, lots of technical work and great fun. Thank you.

Shota Kato.

Hi, I'm Shota Kato. I'm a PhD student in Kyoto University Japan.

My, yeah, I'm not, sorry.

I'm not specialized in natural language processing and my background is chemical engineering and interested in

constructing model automatically. So, I want to, my aim is to build a model automatically. Yeah, that means extract the information of the physical model, such as equation and variance from the literature, and

extract some such information from multiple literature and combine them and build new physical model automatically. That is my objective of research.

Thank you very much. Deborah Mendez.

Hi, I'm Deborah. I'm a PhD student at the University of Manchester in the UK. So my work is focused on probing and understanding how we can apply neural models to mathematical text and hopefully be able to improve the performance on such models.

My plan is to present in our next meeting. So hopefully you'll get to see a bit of my work. Thank you.

Thank you. Tom.

Hi, my name is Tom Weezing. I'm also a PhD candidate in Michael's group. So in Erlang in Germany.

My PhD topic is MathUp, which is a portal for tetrapodal mathematics.

One of the aspects I'm particularly interested in is building search engines over different mathematical or corpora, and that is part of the reason I'm here today I'm interested in hearing results from Dayan and seeing how I can apply them.

Adrian.

Hi, I'm Adrian from the University of Bonn, and I'm also one of the students. And I just feel finished my master's thesis on control of language for mobilization, and I will probably keep working on on that topic for for the next couple years.

And that's sort of the perspective on mathematics and language that I'm coming from.

Okay, Dennis.

Dennis I'm a postdoc in Michael's group in Erlangen.

I have a mathematics background primarily model theory and set theory. My dissertation then was in computer science about formal libraries and building connections between them. And now currently I'm working on the S-Taste system and in particular, an advanced version of that where ideally we get to extract as much semantic information as possible from informal documents.

Yep.