Semantic Search for Mathematics

Stream: Machine Learning for Theorem Proving

[Jason Rute]

I was talking to someone recently and I mentioned how Terry Tao has been asking for some sort of "semantic search" for mathematics for over a decade now. I'm trying to dig up some old posts of his on the topic. The idea is that ideally you should be able to ask a mathematical search engine for a formula or a statement and it should be able to tell you if it is already in the literature. Obviously, you don't just want something which is an exact word for word (or symbol for symbol) match, but also you don't want something which looks similar but is totally not semantically related. I wonder what progress has been made on this over the last decade. Is Google and Google Scholar still about as good as you can get? (Of course Google has also improved over the last decade, but I still think this aspect is lacking.) (Of course the best you can get is still talking to a human expert, which is what MathOverflow and other social networks excel at.)

[Jason Rute]

And of course Terry Tao isn't the only one who has talked about this.

[Jason Rute]

There was an interesting book written about a decade ago on the topic of this and generally building a mathematical digital library Developing a 21st Century Global Library for Mathematics Research. I was asked to be one of the (open) reviewers (because of some comments I left on Tao's blog on the subject). Also, I didn't know who he was at the time, but Yann LeCun (a bigshot in neural networks) was one of the authors. I'd be curious how the ideas have aged over the past decade. It seemed like a hard problem then, and frankly it still seems hard, but maybe slightly more trackable.

[Jason Rute]

Some searching brought up https://approach0.xyz/search/. I've never heard of it before, I wonder if it is any good?

[Junyan Xu]

It's impressive that it comes up with many non-exact matches when I searched for Ramanujan's formula for pi.

[Tom Chen]

Looks like many are (1) change variable name (e.g. n vs k) (2) constant computation (e.g. 26390 vs 58*455), so looks like the engine understands LaTeX and maybe somehow parse it

[Junyan Xu]

There are some discussion under Tao's blogpost in 2009 but Tao didn't participate. There's this talk but not exactly relevant.

[Junyan Xu]

Approach Zero's codebase has been inactive for two years, but in another repo I found a fairly recent paper.

[Junyan Xu]

Some other services that comes to mind, though many are not for math specifically:
Inverse symbolic calculator (fuzzy numerical search for mathematical constants)
SErAPIS for Isabelle from the ALEXANDRIA project
arxiv-sanity (recommends new (machine learning) papers for each tag based on SVMs over tfidf features of paper abstracts)
Semantic Scholar (I use it sparingly and only today learned it's backed by the Allen Institute for AI; another website I consider to be similar, ResearchGate, doesn't brag about use of AI)
Of course there is also the recent Galactica which aims to provide accurate citations but only survived three days; apparently its hallucinations aren't controlled as well as ChatGPT.

[Tyler Josephson ⚛️]

Here’s a paper I came across: https://dl.acm.org/doi/abs/10.1145/3394486.3403056

[Vadim Fomin]

I was the one who was talking to Jason, by the way :) I'm new to this stuff and it really impressed me how the daily working process in a mathematician's life lacks some basic tooling that someone should be able to do. As an NLP Engineer, e. g. someone directly in the profession for making that sort of stuff, I had no idea that there is a need to semantic search in math papers. And given how Terry friggin Tao has been talking about that for a decade, there must be a crying need for it. Given the amazing recent breakthroughs in NLP with large pretrained LMs, there must be some new approaches that haven't been tried yet for this task. Would anyone be up for a big of messing around with LMs for math semantic search?

[Vadim Fomin]

btw, I just talked with an NLP guy who does semantic search and who'd be very interested in building semantic search for math - only we're not sure where to get the data. he also did code search, so maybe we can start with building better semantic search for mathlib? would you folks be interested?

[Zhangir Azerbayev]

Here are some of my quick thoughts.

A nice stepping stone on the way to a search engine for all mathematical knowledge might be a search engine for mathib only. This makes challenges of scale more manageable, and also makes UI/UX easier since we know the goal is always to find the user a formal statement.

My immediate thought would be to train CLIP-style query-value embeddings. At inference time, we'd embed the user's query (which can be natural language, formal, or a mixture of the two), then use a fast nearest neighbors search to match the query embedding against pre-computed value embeddings of mathlib formal statements. Where would we get data? Well one thing we know is that Codex is really good at informalization, and when Codex fails, the prediction is still semantically similar to the correct answer. So we could informalize every theorem in mathlib with Codex, and those pairs give us 100k training examples. Similarly, we could prompt Codex to do other tasks than informalization, for example "Use natural language connectives but mathlib names" or "copy the theorem statement but leave out some hypotheses". This could get us millions of training examples.

I don't know very much about deploying neural nets in synchronous applications, but I expect we'd be using a pretty small neural network and mathlib search volume is pretty low, so we might be able to serve this on a single cloud GPU.

This neural net based approach might not scale to the entire internet, but if we want truly semantic search I don't think we can avoid somehow computing dense vector representations. But perhaps this approach could scale to arXiv + math overflow + stack exchange + journals + ebooks, which is maybe all that matters.

Any thoughts @Yuhuai Tony Wu? This modelling approach is somewhat similar to your team's work on premise selection.

[Vadim Fomin]

I think both a) code search over entire mathlib and b) semantic search over arXiv + math overflow + stack exchange + journals + ebooks would be something worth exploring! Let me ping the guy who does semantic search and code search and who was interested in exploring semantic search for math, and see what he thinks

[Junyan Xu]

Maybe you should first ask in the #general or #maths stream to gather a requirement document or something. From my own experience, I find the mathlib docs search box easy enough to use, and I never use library_search.

[Daniel Selsam]

Zhangir Azerbayev said:

My immediate thought would be to train CLIP-style query-value embeddings.

consider trying https://openai.com/blog/new-and-improved-embedding-model/ before training your own

[Junyan Xu]

Just found this: https://lablab.ai/event/semantic-search-hackathon . Starting tomorrow!

[Martin Dvořák]

Junyan Xu said:

Just found this: https://lablab.ai/event/semantic-search-hackathon . Starting tomorrow!

Any indication there will be people focused on Lean?

[Vadim Fomin]

Hey guys, sorry for disappearing. I was actually thinking I pull you in a call with the semantic search guy? You'd probably help us clarify the use cases for the math semantic search, and we could think together which way to attack the problem, and what can be done? Would you guys be up for a call?

[Johan Commelin]

Why doesn't the semantic search guy join the discussion here on zulip?

[Vadim Fomin]

@Vladimir Orshulevich hey man, this is the Zulip community of the Lean theorem prover, these folks are also interested in semantic search for math. We had a little chat about that, you can see it above. Wanna train a model or something?

[Kevin Buzzard]

The conference at IPAM in Feb on machines and mathematics organised by Terry Tao, Tim Gowers and various people from this Zulip will have a fair bit of lean representation and that very conference is happening because Tao is interested in semantic search in mahematics

[Vadim Fomin]

Btw, can you share use cases for the semantic search, maybe with example queries and responses?

We wanna have an understanding of the goal, and to decide which data to use. (arxiv papers? code search over mathlib?)

[Vladimir Orshulevich]

Hey guys,

Great to be here and have a chance to help with semantic search engine for math!

Following the conversation:
"ada-002" from openAI is cool, but it is paid api. So mb it is reasonable to try it for testing proof-of-concept. But for search service like that I suggest to fine-tune some Salesforce/codegen-{350M, 2B, 6B, 16B}-multi on some pairs . It is pre-trained in similar way. So the problem here is data, everything else I probably know how to implement.

"single cloud GPU"
I've made text-visual and text-audio search services with HNSW index. It's 4-5K qps (inference + search) for single RTX3090 (probably twice with A100). I hope its enough to test. Even though its horizontally scalable.

[Siddhartha Gadgil]

Vadim Fomin said:

Btw, can you share use cases for the semantic search, maybe with example queries and responses?

We wanna have an understanding of the goal, and to decide which data to use. (arxiv papers? code search over mathlib?)

Here is an example of a question I asked chatGPT which it answered incorrectly:

• Is it true that every smooth, closed manifold of dimension at least 3 admits a metric with negative Ricci curvature?

[Siddhartha Gadgil]

This is a deep theorem. Semantic search should find it.

[Siddhartha Gadgil]

Another that I asked chatGPT and it answered incorrectly (answered the wrong question and justified with incorrect logic).

• What are examples of knots that are known not to be ribbon but which may be slice?

For this discussion it does not matter what these mean - they are some properties of knots.

[Siddhartha Gadgil]

chatGPT answered giving examples of knots that are known not to be slice instead. Then claimed it is not known whether they are ribbon.

[Siddhartha Gadgil]

By the result that all ribbon knots are slice, those that are not slice are not ribbon. This is not only a well-known result, but one which chatGPT had stated as background material when answering.

[Junyan Xu]

Is it true that every smooth, closed manifold of dimension at least 3 admits a metric with negative Ricci curvature?

Googling "admit negative ricci curvature" returns the paper of Lohkamp as the first result, which states the result for three-manifolds in the introduction (due to Gao--Yau and Brooks), and the result for dimension >=3 (proven in the paper) is on the second page, but the article is behind JSTOR paywall beyond the first page. I wonder whether Galactica has been trained on sci-hub database ... May need to OCR as well. This info is also avaiable in a math.SE answer though.

What are examples of knots that are known not to be ribbon but which may be slice?

I looked up Knot Atlas and KnotInfo but ribbon-ness seems not to be a field in their databases, so you have to get the information elsewhere (papers and online discussions?).

[Siddhartha Gadgil]

It is in wikipedia including the slice-ribbon conjecture.

[Siddhartha Gadgil]

Another example of a question: what is known about the traces of $2 \times 2$ matrices with integer coefficients with determinant 1

[Kevin Buzzard]

What is known? Presumably the trace can be any integer? Yeah [n,1;-1,0]

[Kevin Buzzard]

Isn't this a calculation/construction rather than something that you can find on the internet? Should one expect an AI to be able to solve this?

[Siddhartha Gadgil]

I asked too simple a question. I believe what I meant to ask was the relation between the traces of $A$, $B$ and the commutator $ABA^{-1}B^{-1}$ for $A$ and $B$ having determinant 1.

[Kevin Buzzard]

And an AI is supposed to be able to answer this?

[Kevin Buzzard]

I don't really know what's in scope

[Siddhartha Gadgil]

An AI is supposed to find papers/books that address this question, and even the statements of theorems within them. That is essentially the definition of "semantic search"

[Martin Dvořák]

AI is not there yet afaik.

[Kevin Lacker]

here's an example for semantic search: "what theorems can tell me when a bunch of lines from the vertices of a triangle to the opposite side intersect?" this is basically an elementary geometry question. it's a bit too advanced for chatgpt, which answers:

There are several theorems that pertain to the intersection of lines drawn from the vertices of a triangle to the opposite side. Here are three such theorems:

The Angle Bisector Theorem states that in any triangle, the line segment drawn from a vertex to the midpoint of the opposite side is bisected by the angle bisector of the angle at that vertex. This means that the line segment is divided into two equal parts by the angle bisector.

The Median Theorem states that in any triangle, the line segment drawn from a vertex to the midpoint of the opposite side is twice as long as the line segment drawn from the midpoint of the opposite side to the midpoint of the opposite side of the triangle.

The Altitude Theorem states that in any triangle, the line drawn from a vertex to the opposite side is perpendicular to that side. This means that the line forms a right angle with the side.

These theorems can help you understand the relationship between the lines drawn from the vertices of a triangle to the opposite side and how they intersect.

none of those are really a direct answer to the question, a better answer i think would be Ceva's theorem - https://en.wikipedia.org/wiki/Ceva%27s_theorem . I bet you could come up with a corpus of questions like this, that could be answered by wikipedia pages. the goal of the semantic search system isn't to directly solve the problem, but just to correctly figure out which pages are the relevant ones, in a way that's better than just googling can do.

[Kevin Buzzard]

Thanks for these explanations: I have a much better understanding of what this phrase means now!

[Sid]

@Kevin Lacker Interestingly, if you pose this question to perplexity.ai, it is able to retrieve Ceva's theorem (https://www.perplexity.ai/?uuid=94ccba12-5e6a-4f3f-b587-e5877fae8bf7). Though its reference of SSS doesn't make sense in context

[Vadim Fomin]

Hey folks,
We have A LOT of arxiv data, but we'd also like to include some math books in the dataset, it would probably make the search more relevant. Do you have any idea where we could scrape some?

[Patrick Johnson]

Vadim Fomin said:

Hey folks,
We have A LOT of arxiv data, but we'd also like to include some math books in the dataset, it would probably make the search more relevant. Do you have any idea where we could scrape some?

Library Genesis and SciHub.

[Vadim Fomin]

A nice suggestion! Is there any chance there is anything open-source (with older books perhaps?)

[Johan Commelin]

Stacks Project and Kerodon are open source.

[Vadim Fomin]

Both look like exactly the kind of thing we're looking for. You see, arxiv papers are nice because there is markup like "Theorem 1", "Lemma 2", and before them, there's some kind of a less formal explanation what's going on ("Let's introduce this idea", "This theorem connects this to that" etc.) - this is likely to be very useful for the semantic search engine. We'd like to find books that are also in this format, there's probably more fundamental stuff that would be good to be able to look up. And both Stacks Project and Kerodon look good for this, only we'd need rather a lot...

[Kaiyu Yang]

https://github.com/rfitzp/Elements

[Junyan Xu]

Project Gutenberg has some math books, e.g. in number theory; not in nice format though

EGA/SGA (algebraic geometry, French): typeset version (Dan Miller should have the SGA TeX source) / scanned version (may be partially superseded by the Stacks project)

J.S. Milne's books and notes in PDF but I guess you can ask him for TeX source

Terry Tao's blogposts were made into several books, so you might as well scrape his blog

Danny Calegari (low-dimensional topology)

Emily Riehl (site down at the moment)

Jacob Lurie's books (are they subsumed by Kerodon?)

[Reid Barton]

Junyan Xu said:

Jacob Lurie's books (are they subsumed by Kerodon?)

They are not (yet).

[Zhangir Azerbayev]

I whipped up a quick demo of mathlib search using the openai embeddings + fast kNN search using Faiss.

https://github.com/zhangir-azerbayev/mathlib-semantic-search

Right now the demo requires you to download ~800mb of pre-computed mathlib embeddings and pay $0.0004 per 1K query tokens.

@Edward Ayers is working on a website with a nice UI that hosts this on the cloud and collects feedback about search results. If the openai embeddings work really well, we could think about integrating them into the mathlib docs and embedding other databases. Even if they don't, we could use the user feedback to create a challenging evaluation set for mathlib semantic search, hopefully with many examples like the one @Kevin Lacker gave.

[Junyan Xu]

https://twitter.com/tomtumiel/status/1611729847700570118

Just built a new website called https://arxivxplorer.com It's a semantic search engine for arXiv papers, and it uses @OpenAI's latest embedding model to find the most relevant papers for your search queries.

- Tom Tumiel (@tomtumiel)

[Martin Dvořák]

Can you show an example prompt that finds a relevant paper but keyword search fails?

[Adam Topaz]

I'm a bit confused as to what this actually does... Anyway, I can't seem to find any search query where the results are meaningful.
For example, searching "prismatic cohomology" doesn't even return arxiv#1905.08229

[Eric Wieser]

(which is the first google result)

[Wojciech Nawrocki]

Adam Topaz said:

I'm a bit confused as to what this actually does... Anyway, I can't seem to find any search query where the results are meaningful.
For example, searching "prismatic cohomology" doesn't even return arxiv#1905.08229

The author doesn't seem to say that explicitly but it possibly only embeds papers in the cs.xyz categories. In a search for "cohomology", all results are tagged with cs.something.

@IntuitMachine @OpenAI It was $40 to embed all the papers in the CS category (about 500k papers)

- Tom Tumiel (@tomtumiel)

[Junyan Xu]

Yeah, if I put https://arxiv.org/abs/1905.08229 into the search box it says it isn't indexed. Sorry for the noise!

[Adam Topaz]

How many papers are in math? I assume more than 500k?

[Siddhartha Gadgil]

Initially I was happy because when I asked it for curvature on graphs it gave very good answers. But then I asked it Riemannian Geometry stuff and it still kept giving curvature on graphs. Looks like CS related stuff overwhelms it.

Seems that filtering by subject area should improve it a lot.

[Zhangir Azerbayev]

I modified my semantic search code to use a way better prompting strategy. Instead of directly embedding the user's input, I'm using Codex to try to autoformalize the user input, then embedding "/-- {user input} -/ \n{codex autoformalization}". Btw, the website is almost done :)

[Junyan Xu]

@Adam Topaz Here's what I got from searching prismatic cohomology on elicit.org: image.png
Bhatt--Scholze appears as the 6th result.
This website seems more oriented towards experimental science, though:
image.png
image.png

[Junyan Xu]

I just discovered that there are now several products that embed a whole paper in PDF format and then allow you to chat with it:

ChatPDF
researchGPT (open-source, requires OpenAI API key)
Explainpaper (which I tried, see below)
Elicit (a bigger product) Demos

Introducing researchGPT An open-source LLM based research assistant that allows you to have a conversation with a research paper! It’s a simple flask app that uses embeddings + gpt-3 to search through the paper and answer questions Try the demo here: http://tinyurl.com/researchgpt https://twitter.com/mukul0x/status/1625673579399446529/video/1

- mukul (@mukul0x)

Maybe we can chat with mathlib as well, using the already computed embeddings?

[Kevin Buzzard]

If we can make a mathlibchat web page that would be super-cool, even if it was mostly rubbish. A lot of what chatGPT produces is rubbish and yet it still continues to be a thing.

[Junyan Xu]

Here are my interactions with Explainpaper around a paper by myself with @David Ang. Apparently, the outputs are generated from semantic searches within the paper. My impression is that the model has an okay understanding of the paper provided to it, and is apparently able to integrate knowledge already present in the model (about mathlib, namespaces, famous mathematical objects or theorems) with new knowledge from the paper, and decipher unexplained acronym (DKA), but sometimes it makes too much connection (class_group pic 1), confuses about relationship between concepts (class_group pic 2, division polynomials), or misunderstands (Friedl's original argument). If the searched word isn't explained in the paper, it may instead output a summary of the whole paper, as in the case of "Borcherds", possibly because the search returns no close match.

image.png image.png image.png image.png image.png image.png
image.png image.png image.png image.png image.png image.png

[Junyan Xu]

I haven't used the chat feature much yet, maybe you can think of nice questions to ask?

[Junyan Xu]

Update: I tried ChatPDF and Explainpaper on another (machine learning) paper, and it turned out that ChatPDF is superior: no need to select text before being able to chat, and more accurate results retrieved.

This flowchat is roughly how Paul Graham GPT chat works, and likely also how ChatPDF works and how Copilot Hub allows you to chat with Steve Jobs and Naval Ravikant. This post explains how to use LlamaIndex to complete the entire workflow. Makes me wonder whether we can use the data from https://www.grothendieckcircle.org/ to chat with Alexander Grothendieck.

@mckaywrigley @paulg The whole flowchart should look like this if I understand it correctly. Thanks to @chuangbo for explaining it. https://twitter.com/dotey/status/1631760676388499460/photo/1

- 宝玉 (@dotey)

[Junyan Xu]

Actually, a more useful thing is to use all Zulip data to create a question-answering chatbot, which should be great in answering beginner questions if not more advanced ones. A lot of businesses were already building customer service bots using ChatGPT, and now the API is open.

We have all data exported to https://github.com/leanprover-community/archive (it's one-month out of date though)

[Zhangir Azerbayev]

Kevin Buzzard said:

If we can make a mathlibchat web page that would be super-cool, even if it was mostly rubbish. A lot of what chatGPT produces is rubbish and yet it still continues to be a thing.

openai recently released the chatgpt api. Adding this as a layer on top of the mathlib semantic search demo would be pretty easy. If we're retrieving ground-truth mathlib declarations, the generating rubbish problem will be mitigated.

I can try implementing this next week.

[Junyan Xu]

commercial solution emerged: https://sitegpt.ai/pricing

[Reid Barton]

I guess someone will make one of these for the arxiv (or one per top-level category).

[Junyan Xu]

Very informative in-depth discussion of vector search/ranking solutions under this tweet: https://twitter.com/jobergum/status/1643187540222959616
And, it looks like Pinecone is something to avoid:
https://twitter.com/kishorelive/status/1646419766641295362?t=8pQPtaHL0trVnHg6zRLJLg
Plus that it can't be run locally and you have to beware of traps:
https://twitter.com/Exploringfornow/status/1642633542189436929

I see that the pgvector extension is mentioned more often in the context of embedding retrieval and semantic search What many seem to overlook is that IVF does not provide very good recall accuracy. Are people really happy with 50% recall for their LLM context retrieval? https://twitter.com/DammianMiller/status/1642878642832429059

- Jo Kristian Bergum (@jobergum)

@NirantK @jobergum @pinecone I would assume so based on language used. "otherwise engage in competitive benchmarking; (iv) disclose the results of any benchmark test of the Hosted Services or the Materials to any third party without Pinecone’s prior written approval; " https://www.pinecone.io/user-agreement/

- Kishore Nallan (@kishorelive)

@jaojiuu @pinecone They charge for every single minute you have an index in your account… meaning from the moment you create an index to the moment you remove it. They advise you switch your index to a collection if not in use, and then switch it back when needed; switching an index from a… https://twitter.com/i/web/status/1642633542189436929

- Yasir (@Exploringfornow)

[Junyan Xu]

You can now chat with mathlib4 at https://wolfia.com/?projectId=bf92ba10-e8c4-4a23-800d-d12afaa98e5e
(I requested them to index the repo and it was done in one day)
However it's almost totally unusable at this moment; looks like it's unable to retrieve anything useful. (I tried "in which file is the parallelogram identity?" "... is the law of cosines?") I suspect they didn't actually index any Lean file. (This is now fixed! See below.)
It works reasonably well for Sage but may be that's because the codebase is mostly Python (+ other common languages).

[Junyan Xu]

Indeed the .lean files were not indexed, which is now fixed, and now Wolfia can generate pretty sensible answers. The files indexed include:
+-----------+-------+
| extension | count |
|-----------+-------|
| json | 3 |
| lean | 3496 |
| md | 4 |
| py | 9 |
| sh | 11 |
| toml | 1 |
| txt | 1 |
| yaml | 1 |
| yml | 13 |
+-----------+-------+
Are there other files that should be indexed?

[Junyan Xu]

LLM explaining mathlib naming convention :) https://wolfia.com/query/01H4J9RZKSXXX11GK57J041H56
but it's weird Wolfia isn't able to retrieve the lemma...

[Junyan Xu]

It looks like there are still some bugs as I can't get Wolfia to find the parallelogram law / polarization identity / law of cosines. Suspecting the containing files aren't indexed and in contact with their CTO Naren. Note that Wolfia uses the open source vector database Milvus.

[Eric Taucher]

Today, I have been catching up on this topic.

Before investing time on creating something was wondering if instead of chatting with a PDF by using ChatGPT plugins for such (ref - put PDF in search bar) if instead someone has tried using the LaTeX or TeX for the paper(s) and is working on such or made available?

I found that using ChatOCR failed to interpret the typing rules from a PDF (ref).

So conducted a simple test to determine if ChatGPT could understand TeX for a paper containing typing rules. When provided just the TeX code for the typing rules of the image to ChatGPT, it was able to generate a coherent reply (ref)."

image.png

Completion

The figure you provided presents a set of typing rules for the \gpml type system. These rules define how different patterns and expressions are typed in the system. Let’s go through each rule:

The first two rules state that a node or an arc literal with or without a label is typed as a node or an edge, respectively.

The third rule states that if a variable x is not bound in the pattern (\pat), then x can be restricted to a path and typed as a path (\tpath).

The fourth rule states that if a pattern \pat is typed as z of type \tau, then the pattern \pat\quantlit{n..m} is typed as z of type List(\tau).

The fifth and sixth rules deal with restricting patterns. If a pattern \pat is typed as z of type \tau, then the pattern \restrictor\ \pat is also typed as z of type \tau.

The seventh rule states that if a pattern \pat is typed as x of type \tau, where \tau is either a node or an edge, then the expression x.a=c is typed as a Boolean (\tbool).

The eighth rule states that if a pattern \pat is typed as x of type \tau and another pattern y is typed as y of type \tau', where both \tau and \tau' are either nodes or edges, then the expression x.a=y.b is typed as a Boolean (\tbool).

The ninth, tenth, eleventh, and twelfth rules deal with Boolean operations. They state that if patterns or expressions \pat and \theta are typed as Boolean values, then the conjunction (\wedge), disjunction (\vee), negation (\neg), and conditional (\condlit{\theta}) expressions are also typed as Booleans.

The thirteenth rule states that if patterns \pat_1 and \pat_2 are both typed as z of type \tau, then the pattern \pat_1 + \pat_2 is also typed as z of type \tau.

The fourteenth, fifteenth, and sixteenth rules deal with patterns that include optional values. They specify how patterns with optional values are typed based on the presence or absence of the value.

The seventeenth, eighteenth, and nineteenth rules deal with concatenating patterns and expressions. They specify the typing for the concatenation operator (,). If patterns or expressions \pat_1 and \pat_2 are typed as z of type \tau, then \pat_1 \, \pat_2 is also typed as z of type \tau. Additionally, if the variable z is not bound in either \pat_1 or \pat_2, then the typing remains the same.

The twentieth, twenty-first, and twenty-second rules deal with concatenating queries (Q_1 and Q_2). They specify the typing for the concatenation operator (,). If queries Q_1 and Q_2 are both typed as z of type \tau, then Q_1 , Q_2 is also typed as z of type \tau. Additionally, if the variable z is not bound in either Q_1 or Q_2, then the typing remains the same.

These rules define the typing behavior of various patterns and expressions in the \gpml type system.

[Lev Stambler]

Does anyone know what happened to Wolfia? I was finding it quite useful, but it seems to not be up.

[Junyan Xu]

Unfortunately it's discontinued. Here's what I got from their CTO:

We've realized that while people love using the service, no one really is willing to pay for it (in its current state, at least).
Here's a few products out solving similar problems:
https://about.sourcegraph.com/cody
https://mutable.ai/
https://www.cursor.so/

[Lev Stambler]

Junyan Xu said:

Unfortunately it's discontinued. Here's what I got from their CTO:

We've realized that while people love using the service, no one really is willing to pay for it (in its current state, at least).
Here's a few products out solving similar problems:
https://about.sourcegraph.com/cody
https://mutable.ai/
https://www.cursor.so/

Oh okay. Makes sense. It is a bummer though