Discussion: Sequencelib

Stream: general

[Eric Taucher]

Walter Moreira said:

We are very open to suggestions as well.

What timing, currently creating an MCP server for OEIS.

B-files are the problem, AI wants to import really large ones into the conversation, making progress, think guardrails.

If/when I get it working it will most likely be MIT license so feel free to learn from it, use it, etc.

[Joe Stubbs]

Thanks @Eric Taucher , we'll definitely be interested to check it out once you get it working.

[Eric Taucher]

(deleted)

[Notification Bot]

3 messages were moved here from #announce > Sequencelib: a platform for formalizing sequences from OEIS by Mario Carneiro.

[Lode Vermeulen]

(the original discussion link in the announcement post is wrong)

[Jz Pan]

I think it's best if there is a script collecting all sequences we have in the page https://provables.github.io/sequencelib/docs/Sequencelib.html.

[Walter Moreira]

The current setup collects the sequences in the main page (https://provables.github.io/sequencelib/), where the index is generated by the tagged sequences and the titles are pulled from the OEIS site. Do you feel it would be useful to display them in the docs page as well?

[Jz Pan]

Walter Moreira said:

Do you feel it would be useful to display them in the docs page as well?

Yes I think so.

[Walter Moreira]

Thank you for that suggestion. We updated the script to display the index both in the main website and in the docs page: https://provables.github.io/sequencelib/docs/Sequencelib/Basic.html

[Jz Pan]

Thank you! But do you think it's better to add them to https://provables.github.io/sequencelib/docs/Sequencelib.html? Since Basic does not import any of the actual definition of sequences, but Sequencelib imports all of them. I think maybe you can introduce a meta command to insert all sequences imported to module docstring.

[Walter Moreira]

Good point. I updated the script to display the index in Sequencelib.html, instead of Basic.html. It looks nicer in the url and one can see all the imports for the package.

[Eric Taucher]

(deleted)