Now that we’ve gotten quite familiar with Org Mode things, it could be good to revisit previous work (by some of us) with Arxana — and to see what it might have to offer here.

Basic questions: who cares about this, and what does Arxana do?

There are some simple tasks that aren’t entirely obvious how to solve in Org Mode. Suppose for example that I want to browse all of the pages marked with #+roam_tags: HL. Well, right now I’d probably have to write a custom exporter just to look at that material. But supposing that I actually wanted to edit all that material in one place, then press save, and have the edited text reappear in the original source locations? You might think that this would be solved with the org-transclusion package, but actually the transcluded text can’t just be edited directly with that package. It might be better to think in terms of real-time shared editing of the text from multiple people, as with crdt.el, just sourcing the contents from different existing files. Well, Arxana did something a little bit like that, although less nicely. It also tried to model everything as a fancy kind of graph.


Arxana is somewhat similar to Atomspace. It would be possible to create a (Clojure) backend that’s linked with Crux or some other graph database.

When we left off working on Arxana in 2017, we made a few notes. Maybe it could be applied to something interesting for which we could get a grant. Below, is some of the future work (circa FARM 2017).

The code is stored in (with the latest in the mob branch). There’s some written propaganda about the project at

Mob branch on

Incidentally, if you want to contribute anonymously, info on how to do that is here:

You can review commits to the mob branch here:

2021 report: Dusting off the Tome

I’m starting to revive Arxana for use in grant applications (targeting EPSRC: Mathematical Sciences Small Grants). As I go along I want to better understand how the old versions of the code works, and better understand the use cases for which something like Arxana could be relevant.

Use case: Edit transcluded filesusecase

  • I have a bunch of org files managed by Org Roam

  • I also have code for pulling them together into one big Org file.

  • I'd like to be able to edit the big Org file, and have the changes flow back to all of the underlying Org Roam files without having to think about saving or copying and pasting.

This particular example should in principle be doable with org-transclusion, but looking into it a bit more, that’s not actually how the existing implementation works:

Transcluded contents are read-only. To edit them, useorg-transclusion-open-edit-src-buffer-at-point command. By default, it is bound to C-c n e in org-transclusion-mode-map (modify the keybinding as you prefer).

On the other hand, a limited working version of the workflow is afforded by M-x occur followed by e, which allows editing the lines where a given word occurs. But this is much more limited than a full-transclusion based workflow.

Probe: Get Arxana 2005 runningprobe

I got Arxana 2005 running again, with minor updates to the code. This recipe now works to get a first look at what’s going on.

  1. Find sbdm4cbpp.tex.

  2. Evaluate the code block in the section called “Preface”.

  3. Enter C-; d a section RET to browse a list of major sections (change to the *Generic List* buffer if it doesn’t pop up automatically). Hit RET in the *Generic List* buffer to view listed contents.

  4. Follow colorful links in the Main Article Display or Scholia Display buffers with C-; f.

  5. Type C-; C-h to list other keyboard commands.

So far, nothing we haven’t seen in Org Mode.

In particular, even though the system imports bits of sbdm4cbpp.tex as the demo, it’s not clear that it actually allows the user edit these pieces and save them back into the source (as described above). Exploring some of the other commands

Adding a scholium and editing an article

It was possible to create a scholium about a given article with C-; m p, i.e,. make-scholium-about-part-of-current-article, then edit the article and commit changes with C-; c, i.e., commit-edits, and notice the text moving around appropriately. So, that’s a little bit new.

Old agenda for developing Arxana (circa our FARM paper)

Immediate upcoming: Before September 3-9 ICFP conference, focusing on our demo

Clean up namespaces of functionsmaintenance

E.g. write honey:add-nema instead of add-nema.

find the generic interface layer and put it in its own filemaintenance

Sketched in, but let's make sure it's consistent.

Assemble/disassemble a buffer from/to distributed storagedemoscheme

While not needed for our FARM demo, this could be useful for the Scheme demo because it makes a relatively convincing case. And furthermore this would be good as user facility and for us as we continue working on the project.

  • E.g., related work of arxana-merge merge automatically.

Write a basic IATCD evaluator to load Listing 1 stuffdemofarm

What is a better name for IATCD? ;-)

This is just at the level of moving data around - specifically turning s-expressions into triples.

Use scholium-based programs to run Listing 2demofarm

This is a minimal working implementation of what we talk about in the paper.

How do inferential connections work (I/R, I/E, etc.)?demofarm

E.g. fig. 7 of Lytinen.

This is just for exposition, when talking about prior art it would be nice to know how they did it.

  • links between basic CD's

    • e.g., joe communicated the IP address to ray, by talking, so that ray could get on the server

Next steps: Paper for IJCAI 2018

IJCAI 2018: Write up applications to mathematicsplatform

Possibly for IJCAI/ECAI. Papers due January 2018? To take place July 13-19, 2018

Revisit history of AI

  • How has AI been applied (games are relatively closed, mathematics is more complex, the world is still more complex)

  • Is ethics more complex than biology?

  • Compare some thinking in the history of cultural thought — Mosaic-Axial-present

  • 2500 years ago; city-states and prose-literacy.

  • Cf. the Sloterdijk Shadow of Mt Sinai

Demo the system walking through the steps of a proof like GCP or MPM.

Demo with APM prelim problems

This might be a "future work" section for this paper.

Demo with APM-Xi content

Show interface with types.

  • E.g. APM-Xi style formulations of category theory definitons could be salient to work with.

Next steps: Paper for ICFP 2018

BACK ICFP 2018: Logic programming like Reasoned Schemer but for hypergraphsplatform

  • To start with, read the actual reasoned schemer

  • And we could apply it to our project.

  • We could make an org mode notebook of the thing

  • Maybe expand the ideas ‘what does this do’ with other exercises

  • When we get it going we might get in touch with Friedman and Byrd, and explore

  • How would it met with neural nets

  • Maybe look at this in relationship to

Possibly submit to ICFP. Papers due Fri 16 Mar 2018. Event to take place in St. Louis, Missouri, United States, to take place late September.

Fuzzy search to retrieve loose matches and analogies

Write a simple user language and an interface that generates triplets/quintuplets

Can the system come up with answers to new, basic, questions?

  • Inspired by Nuamah et al's geography examples

  • Simple comparisons, like, how does this concept relate to that concept? We informally talk about this as ``analogy'' between concepts. But...

Foldable views (like in Org mode) so that people can browse proofs

  • This may come after the May submission

  • Folding and unfolding the definitions of terms in something like an APM context is relevant example. Just `unpacking' terms.

  • Note that there is some relevant prior work in the "Wikum" paper of Amy Zhang et al

Other next steps: from the Future Work section of our FARM paper

This could potentially be used as the basis of an ERC fellowship proposal. The "2018" version of the call was released August 3 2017, and is due October 17 2017. Presumably the "2019" version of the call will be run on a similar timeline. A long PDF describing the current call is here: =h2020-guide18-erc-stg-cog_en.pdf=

Formal proof

Demo the system walking through the steps of a proof like GCP or MPM.

If we keep at it, might have this ready by January, in time for an IJCAI paper.

Refine both representations and reasoning aspects.

Integrate external computer algebra / proof checking systems.

Embodiment and cognitive science

Build on CD theory to reason about embodied intuitions in geometric problems, integrate with Lakoff and Núñez's conceptual metaphors \cite{kaliszyk2014developing-misc}.

Linguistics and NLP

Integrate parsers to generate IATC+CD automatically.

Use these models to seed statistical machine learning, e.g., expanding on the work of Kaliszyk et al who ascertained the frequency of various schematic usages like ``let \(X\) be a \(Y\)'' in a specific corpus of proofs.

Machine learning

Integrate with knowledge bases of mathematical terms and frequency data (as above).

Model Stack Exchange dialogues, in parallel with the work done on Reddit discussions \cite{zhang2017characterizing}.

Build a system with multiple agents that ``converse with each other to sharpen their wits'' \cite{heretical-theory}.