ABSTRACT. The House of Graphs is an online database of graphs which can be accessed at https://houseofgraphs.org/. It serves as a central repository for complete lists of graphs for various graph classes. However, its main feature is a searchable database of so-called "interesting" graphs. The development of the original House of Graphs started in 2010 and it was completely rebuilt in 2021-2022. Each graph in the database is accompanied by a significant amount of meta-data such as a name, drawings, precomputed graph invariants, and comments. Given this volume of information and the importance of reliability in the scientific world, robust data management is essential to ensure accuracy and consistency across the database. In this article, we therefore focus on knowledge management in the House of Graphs and describe the inner workings of the House of Graphs and how we ensure that its data is coherent, qualitative and stable.

ABSTRACT. Graphs, maps on surfaces, and abstract polytopes are related combinatorial structures that tend to be studied by different communities using their own tools and databases. Maniplexes provide a unifying framework that captures all of them. A single database built around maniplexes would help researchers recognize shared structures and translate results across fields. Here we present a compact, interoperable format for storing maniplexes as edge-labeled graphs, designed with such a database in mind. As a first step, we connect two existing datasets of regular 4-maniplexes to the House of Graphs and to Potočnik's tetravalent graph censuses, using canonical forms of their flag graphs, 1-skeleton graphs, and 1-coskeleton graphs.

ABSTRACT. We introduce a combinatorial rewriting model for origami that provides a formal foundation for describing folding processes. While origami constructions are inherently geometric, many of their essential features—such as face adjacency, layering, and the evolution of structure through folds— can be captured at a combinatorial level.

We define an abstract origami structure consisting of a finite set of faces equipped with adjacency and layering relations, and formalize folding as a sequence of rewrite steps composed of face division and face rotation. The update of the layering relation is defined by combining combinatorial rules with geometric conditions, in particular overlap relations induced by folding. This interaction between discrete structure and geometric constraints is central to the model.

Our approach is related to earlier work on algebraic graph rewriting in origami~\ref{see-at-the-abstract}, but the model proposed here introduces a new structural formulation and operational semantics that are more directly aligned with the current design of the Eos (e-origami) system. In particular, we formulate well-formedness as a global invariant and clarify how rewrite steps preserve consistent layering while allowing complex geometric interactions.

The proposed framework provides a basis for formal reasoning about origami constructions and offers a bridge between symbolic computation and geometric modeling. It also opens the way to systematic analysis, verification, and implementation of origami processes within computational systems.

------ Reference: Tetsuo Ida, Hidekazu Takahashi: Origami fold as algebraic graph rewriting. J. Symb. Comput. 45(4): 393-413 (2010)

------

ABSTRACT. Integer sequences in the OEIS span values from single-digit constants to astronomical factorials and exponentials, making prediction challenging for standard tokenised models that cannot handle out-of-vocabulary values or exploit periodic arithmetic structure. We present IntSeqBERT, a dual-stream Transformer encoder for masked integer-sequence modelling on OEIS. Each sequence element is encoded along two complementary axes: a continuous log-scale magnitude embedding and sin/cos modulo embeddings for 100 residues (moduli 2 to 101), fused via FiLM. Three prediction heads (magnitude regression, sign classification, and modulo prediction for 100 moduli) are trained jointly on 274,705 OEIS sequences. At the Large scale (91.5M parameters), IntSeqBERT achieves 95.85% magnitude accuracy and 50.38% Mean Modulo Accuracy (MMA) on the test set, outperforming a standard tokenised Transformer baseline by +8.9 pt and +4.5 pt, respectively. An ablation removing the modulo stream confirms it accounts for +15.2 pt of the MMA gain and contributes an additional +6.2 pt to magnitude accuracy. A probabilistic Chinese Remainder Theorem (CRT)-based Solver converts the model's predictions into concrete integers, yielding a 7.4-fold improvement in next-term prediction over the tokenised-Transformer baseline (Top-1: 19.09% vs. 2.59%). Modulo spectrum analysis reveals a strong negative correlation between Normalised Information Gain (NIG) and Euler's totient ratio phi(m)/m (r = -0.851, p < 10^{-28}), providing empirical evidence that composite moduli capture OEIS arithmetic structure more efficiently via CRT aggregation.

ABSTRACT. Mathematical expressions may contain undefined terms, and mathematicians employ a lot of ingenuity to handle them: for example, manipulating limits before they are shown to exist -- without introducing inconsistencies -- or yet avoiding redundant existence condition checks in clever ways. Teaching how to do so is an important topic in undergraduate math, as students should quickly become familiar with these methodologies, and capturing them formally is complex. Whereas ad-hoc logics have been developed for this task, interactive provers and mathematical tools that we would also like to employ in education are based on a total logic, where undefined terms can only be encoded in a non-totally satisfactory way. In this paper, we implement a toolbox to encode partial terms, strict functions and predicates in type theory, partially automating the reasoning about definedness. Moreover, we capture some of the ingenuity of mathematicians in postponing and minimizing the need to check terms to be defined.

ABSTRACT. Mathswitch is an open-source project that imports mathematical concept records from sources such as WikiData, Wikipedia, MathWorld, Encyclopedia of Mathematics, nLab, ProofWiki, and Agda-Unimath, and links records that refer to the same concept. It does not reorganize or redefine the imported content; each source retains its own structure. The current focus is on importing high-quality concept data from WikiData and the resources it links to, with plans to expand to further sources and better concept linking. Because the concept set is approximated through queries over WikiData's collaboratively edited graph, the imported data is noisy: some items are non-mathematical, while others are ambiguous. In this paper, we test whether a voting ensemble of LLM judges can filter this noise. We evaluate it on WikiData items with known MathWorld identifiers as a positive control, and examine how classification changes when database identifiers are removed from context. We then inspect the cases where the judges disagree with MathWorld and group these disagreements into three categories (degenerate descriptions, narrow scope bias, and editorial-scope mismatches) that suggest different remediation strategies.

ABSTRACT. We consider the problem of identifying subsets of variables that are likely to participate in an underlying (possibly unknown) relationship within a mathematical database. We treat each variable as a target and assess the predictive relevance of all others using a diverse collection of machine learning algorithms. Aggregating multiple measures of predictive importance yields a weighted network of pairwise dependencies among variables. We conjecture that groups of variables with high mutual predictive importance correspond to candidates for meaningful mathematical relationships. We test this hypothesis on a curated subset of integer sequences from the OEIS with known interdependencies. Our results show that when algorithms are trained on sufficiently long prefixes of the sequences, the method identifies variables involved in known relationships and suggests candidate relationships, achieving an Area Under the Precision–Recall Curve (AUPRC) that is more than four times that of a random baseline.

ABSTRACT. While datasets of mathematical objects may provide precomputed properties of said objects and thus save the user from expensive computations, verifying their correctness could be as expensive, as in the worst case we might have to recompute from scratch. Often we can mitigate this problem by providing certificates which make it possible to verify the properties efficiently. Such certificates may also help import the objects from the dataset into a proof assistant.

We have designed a certificate for the automorphism group of a graph that efficiently certifies the fact that a given permutation group is the full automorphism group of a given graph. We computed the certificates for the combined censuses of connected cubic vertex-transitive graphs on up to 1280 vertices by Potočnik, Spiga and Verret, and of connected cubic symmetric graphs on up to 2048 vertices by Conder. The censuses are available in the DiscreteZOO database. Our certificates can be used to verify further symmetry properties of the graphs, such as their vertex- and arc-transitivity.