Mathematical Software – ICMS 2018

In this paper, we present ÁTAME, an assertion-based program specialization tool for the multi-paradigm language Maude. The program specializer ÁTAME takes as input a set $$\mathcal{A}$$A of system assertions that model the expected program behavior plus a Maude program $$\mathcal{R}$$R to be specialized that might violate some of the assertions in $$\mathcal{A}$$A. The outcome of the tool is a safe program refinement $$\mathcal{R}'$$R′ of $$\mathcal{R}$$R in which every computation is a good run, i.e., it satisfies the assertions in $$\mathcal{A}$$A. The specialization technique encoded in is fully automatic and ensures that no good run of $$\mathcal{R}$$R is removed from $$\mathcal{R}'$$R′, while the number of bad runs is reduced to zero. We demonstrate the tool capabilities by specializing an overly general nondeterministic dam controller to fulfill a safety policy given by a set of system assertions.

Motivated by the ever-increasing difficulty of proofs of security and correctness, cryptographers have drawn inspiration from the more general software and hardware verification communities and integrated formal methods tools and techniques into their workflows. Though this practice of computer-aided cryptography is still comparatively young, it has spawned a number of automated cryptographic analysis tools. These tools can be categorized in one of two ways: tools focused on theoretical, or “provable,” aspects of security; and tools focused on verifying more practical implementation details. This paper discusses our motivation for, and early work towards, finding an approachable middle ground of the current cryptographic tool spectrum.

In this paper, we propose a new version of the Lagrange interpolation applied to binary permutation polynomials and, more generally, permutation polynomials over prime power modular rings. We discuss its application to obfuscation and reverse engineering.

Numerical algebraic geometry provides tools for approximating solutions of polynomial systems. One such tool is the parameter homotopy, which can be an extremely efficient method to solve numerous polynomial systems that differ only in coefficients, not monomials. This technique is frequently used for solving a parameterized family of polynomial systems at multiple parameter values. This article describes Paramotopy, a parallel, optimized implementation of this technique, making use of the Bertini software package. The novel features of this implementation include allowing for the simultaneous solutions of arbitrary polynomial systems in a parameterized family on an automatically generated or manually provided mesh in the parameter space of coefficients, front ends and back ends that are easily specialized to particular classes of problems, and adaptive techniques for solving polynomial systems near singular points in the parameter space.

There have been various efforts to collect certain mathematical results into searchable databases. In this paper, we present DiscreteZOO: a repository and a fingerprint database for discrete mathematical objects. At the moment, it hosts collections of vertex-transitive graphs and maniplexes, which are a common generalisation of maps and abstract polytopes. The project encompasses a tool for handling and maintaining collections of objects, as well as a website and SageMath package for interacting with the database. The project aims to become a general platform to make collections of mathematical objects easier to publish and access.

We offer a public-key encryption protocol where decryption of a single bit by a legitimate party is correct with probability p that is greater than 1/2 but less than 1. At the same time, a computationally unbounded (passive) adversary correctly recovers the transmitted bit with probability exactly 1/2.

We present two algorithms to classify cubic surfaces over a finite fields. An implementation in the programming system Orbiter will be described.

Many problems in Combinatorics and related fields reduce to the problem of computing orbits of groups acting on finite sets. One of the techniques is known under the name Snakes and Ladders. We offer the alternate name poset classification algorithm. We will describe this technique and compare the performance on example problems.

We discuss an algorithm to search for rainbow cliques in vertex-colored graphs. This algorithm is a generalization of the Bron-Kerbosch algorithm to search for maximal cliques in graphs. As an application, we describe a larger algorithm to classify a certain type of geometric-combinatorial objects called BLT-sets. We report on the classification of BLT-sets of order 71.

We present our implementation of an algorithm which functions as a numerical oracle for the Newton polytope of a hypersurface in the Macaulay2 package NumericalNP.m2. To showcase this software, we investigate the Newton polytope of both a hypersurface coming from algebraic vision and the classical Lüroth invariant.

The problem of detecting when two moving ellipsoids overlap is of interest to robotics, CAD/CAM, computer animation, etc. By analysing symbolically the sign of the real roots of the characteristic polynomial of the pencil defined by two ellipsoids $$\mathcal {A}$$A and $$\mathcal {B}$$B we use and analyse the new closed formulae introduced in [9] characterising when $$\mathcal {A}$$A and $$\mathcal {B}$$B overlap, are separate and touch each other externally for determining the interference of two moving ellipsoids. These formulae involves a minimal set of polynomial inequalities depending only on the entries of the matrices A and B (defining the ellipsoids $$\mathcal {A}$$A and $$\mathcal {B}$$B), need only to compute the characteristic polynomial of the pencil defined by A and B and do not require the computation of the intersection points between them. This characterisation provides a new approach for exact collision detection of two moving ellipsoids since the analysis of the univariate polynomials (depending on the time) in the previously mentioned formulae provides the collision events between them.

Given a finite set of distinct points, a separator family is a set of polynomials, each one corresponding to a point of the given set, such that each of them takes value one at the corresponding point, whereas it vanishes at any other point of the set. Separator polynomials are fundamental building blocks for polynomial interpolation and they can be employed in several practical applications. Ceria and Mora recently developed a new algorithm for squarefree separator polynomials. The algorithm employs as a tool the point trie structure, first defined by Felszeghy-Ráth-Rónyai in their Lex game algorithm, which gives a compact representation of the relations among the points’ coordinates. In this paper, we propose a fast implementation in C of the aforementioned algorithm, based on an efficient storing and visiting of the point trie. We complete the implementation with tests on some sets of points, giving different configurations of the corresponding tries.

The computation of intersection points of generic tropical hyper-surfaces is a fundamental problem in computational algebraic geometry. An efficient algorithm for solving this problem will be a basic building block in many higher level algorithms for studying tropical varieties, computing mixed volume, enumerating mixed cells, constructing polyhedral homotopies, etc. libtropicon is a library for computing intersection points of generic tropical hyper-surfaces that provides a unified framework where the several conceptually opposite approaches coexist and complement one another. In particular, great efficiency is achieve by the data cross-feeding of the “pivoting” and the “elimination” step — data by-product generated by the pivoting step is selectively saved to bootstrap the elimination step, and vice versa. The core algorithm is designed to be naturally parallel and highly scalable, and the implementation directly supports multi-core architectures, computer clusters, and GPUs based on CUDA or ROCm/OpenCL technology. Many-core architectures such as Intel Xeon Phi are also partially supported. This library also includes interface layers that allows it to be tightly integrated into the existing ecosystem of software in computational algebraic geometry.

We present a new method to plot planar implicit curve in a given box $$B \in {\mathbb {R}}^2$$B∈R2. Based on analyzing the geometry of the level sets of the given function, following the points with local maximal (or minimal) curvatures on the level sets, we compute points on each components of the given function in box B and trace each component to plot the curve. We also used this method to find real zeros of bivariate function systems in a given box. The experiments shows that our implementation works well. It works for polynomials with degrees more than 10,000. It also works for non-polynomial case.

Management of software information is difficult for various reasons. First, software typically cannot be reduced to a single object: information about software is an aggregate of software code, APIs, documentation, installations guides, tutorials, user interfaces, test data, dependencies on hardware and other software, etc. Moreover, secondary information about software, especially use cases and experience with employing the software, is important to communicate. Second, typically named software, which we term here a ‘software product’, is taken to stand for all versions of the software which can have different features and properties and may produced different results from the same input data. Software production is a dynamic process and software development is, increasingly, widely distributed. Therefore GitHub, GitLab, Bitbucket and other platforms for sharing are used. Information about software is alos provided in different locations, on websites, repositories, portals, etc. Each resource provides information about software from a particular point of view, but the information is often not linked together. Therefore swMATH has developed a conception which covers portals and a search engines for mathematical software, persistent and citable landing pages for specific software, and a method for software archiving. Based on the publication-based approach, swMATH collects and analyses semi-automatically the existing information about mathematical software found on the Web and makes it available in a user-oriented way. In the talk, we discuss recent extensions of the swMATH conception. We focus on the connection between the swMATH landing pages and different repositories for software.

We describe the algebraic-geometric modeling platform Axl, which provides tools for the manipulation, computation and visualisation of semi-algebraic models. This includes meshes, basic geometric objects such as spheres, cylinders, cones, ellipsoids, torus, piecewise polynomial parameterisations of curves, surfaces or volumes such as b-spline parameterisations, as well as algebraic curves and surfaces defined by polynomial equations. Moreover, Axl provides algorithms for processing these geometric representations, such as computing intersection loci (points, curves) of parametric models, singularities of algebraic curves or surfaces, certified topology of curves and surfaces, etc.We present its main features and describe its generic extension mechanism, which allows one to define new data types and new processes on the data, which benefit from automatic visualisation and interaction facilities. The application capacities of the software are illustrated by short descriptions of plugins on algebraic curves and surfaces and on splines for Isogeometric Analysis.

Group exponentiation is an important and expensive operation used in many public-key cryptosystems and, more generally, cryptographic protocols. To expand the applicability of these solutions to computationally weaker devices, it has been advocated that this operation is delegated from a computationally weaker client to a computationally stronger server. Solving this problem in the case of a single, possibly malicious, server, has remained open since a formal model was introduced in [8]. Recently, in [10] we proposed practical and secure solutions applicable to a class of cyclic groups. In this paper, we propose efficient and secure solutions applicable to a large class of multiplicative groups, possibly beyond groups currently subject to quantum cryptanalysis attacks.

We present a classifier for the Mathematics Subject Classification (MSC) system, combining techniques in unsupervised learning such as nearest neighbors, and supervised learning such as neural networks. We will discuss the challenges presented in the classification task, such as the large number of possible classes, many with overlapping scope; and describe the data processing and experimental methodologies employed.

We present a recommender system covering math and math physics papers from the arXiv, to assist researchers to quickly retrieve theorems and discover similar results from this vast corpus. The retrieval aims to discover not just syntactic, but also semantic similarity. We will discuss the challenges encountered and the experimental methodologies used.

While there has been some discussion on how Symbolic Computation could be used for AI there is little literature on applications in the other direction. However, recent results for quantifier elimination suggest that, given enough example problems, there is scope for machine learning tools like Support Vector Machines to improve the performance of Computer Algebra Systems. We survey the author’s own work and similar applications for other mathematical software.It may seem that the inherently probabilistic nature of machine learning tools would invalidate the exact results prized by mathematical software. However, algorithms and implementations often come with a range of choices which have no effect on the mathematical correctness of the end result but a great effect on the resources required to find it, and thus here, machine learning can have a significant impact.

Mathematical proofs will play a crucial role in building a universal digital mathematics library (UDML). Traditional and formal style proofs do not adequately fulfill all the purposes that mathematical proofs have. We propose a new style of proof that fulfills seven purposes of mathematical proofs. We believe this style of proof is needed to build a highly interconnected UDML.

A major area in neuroscience research is the study of how the brain processes spatial information. Neurons in the brain represent external stimuli via neural codes. These codes often arise from stereotyped stimulus-response maps, associating to each neuron a convex receptive field. An important problem consists in determining what stimulus space features can be extracted directly from a neural code. The neural ideal is an algebraic object that encodes the full combinatorial data of a neural code. This ideal can be expressed in a canonical form that directly translates to a minimal description of the receptive field structure intrinsic to the code. Here, we describe a SageMath package that contains several algorithms related to the canonical form of a neural ideal.

In this paper, we introduce the concept of universal Gröbner basis for a parametric polynomial ideal. In this direction, we present a new algorithm, called UGS, which takes as input a finite set of parametric polynomials and outputs a universal Gröbner system for the ideal generated by input polynomials, by decomposing the space of parameters into a finite set of parametric cells and for each cell associating a finite set of parametric polynomials which is a universal Gröbner basis for the ideal corresponding to that cell. Indeed, for each values of parameters satisfying a condition set, the corresponding polynomial set forms a universal Gröbner basis for the ideal. Our method relies on the parametric variant of the Gröbner basis conversion and also on the PGBMain algorithm due to Kapur et al. to compute parametric Gröbner bases. The proposed UGS algorithm has been implemented in Maple-Sage and its performance is investigated through an example.

Computational tools in numerical algebraic geometry can be used to numerically approximate solutions to a system of polynomial equations. If the system is well-constrained (i.e., square), Newton’s method is locally quadratically convergent near each nonsingular solution. In such cases, Smale’s alpha theory can be used to certify that a given point is in the quadratic convergence basin of some solution. This was extended to certifiably determine the reality of the corresponding solution when the polynomial system is real. Using the theory of Newton-invariant sets, we certifiably decide the reality of projections of solutions. We apply this method to certifiably count the number of real and totally real tritangent planes for instances of curves of genus 4.

Many search problems over Boolean variables can be formulated in terms of satisfiability of a set of clauses or solving a system of Boolean polynomials. On one hand, there exists a great variety of software coming from different areas such as commutative algebra, SAT or SMT, that can be used to tackle these instances. On the other hand, their approaches to inferring new constraints vary and seem to be complementary to each other. For instance, compare the handling of XOR constraints in SAT solvers to that in computer algebra systems. We present a C++ implementation of a platform that combines the power of the Boolean Border Basis Algorithm (BBBA) with a CDCL SAT solver in a portfolio-based fashion. Instead of building a complete fusion or a theory solver for a particular problem, both solvers work independently and interact through a communication interface. Hence a greater degree of flexibility is achieved. The SAT solver antom, which is currently used in the integration, can be easily replaced by any other CDCL solver. Altogether, this is the first open-source implementation of the BBBA and its combination with a SAT solver.

In this paper we discuss the Hidden Subgroup Problem (HSP) in relation to post-quantum cryptography. We review the relationship between HSP and other computational problems, discuss an optimal solution method, and review results about the quantum complexity of HSP. We also overview some platforms for group-based cryptosystems. Notably, efficient algorithms for solving HSP in the proposed infinite group platforms are not yet known.

Previous work on orbital graphs has shown that they are a powerful pruning tool in backtrack algorithms. In this article we consider a few questions that are relevant from this perspective, focussing on properties of orbital graphs that can be detected by an efficient algorithm. Roughly speaking, the challenge is to decide when to use orbital graphs and, possibly, how to choose a “best” orbital graph, and to make this decision early in the algorithm at low computational costs. In this note we discuss how to decide whether or not a given digraph is an orbital graph for some group and what groups are recognisable by their orbital graphs (or even just one orbital graph). We approach these problems from a theoretical point of view.

We describe Ccluster, a software for computing natural $$\varepsilon $$ε-clusters of complex roots in a given box of the complex plane. This algorithm from Becker et al. (2016) is near-optimal when applied to the benchmark problem of isolating all complex roots of an integer polynomial. It is one of the first implementations of a near-optimal algorithm for complex roots. We describe some low level techniques for speeding up the algorithm. Its performance is compared with the well-known MPSolve library and Maple.

We propose an extension of the automated theorem prover E by the weighted path ordering. Weighted path ordering is theoretically stronger than all the orderings used in E-prover, however its parametrization is more involved than those normally used in automated reasoning. In particular, it depends on a term algebra. We discuss how the parameters for the ordering can be proposed automatically for particular theorem proving problem strategies. We integrate the ordering in E-prover and perform an evaluation on the standard theorem proving benchmarks. The ordering is complementary to the ones used in E prover so far.

We present an implementation of arbitrary-precision numerical integration with rigorous error bounds in the Arb library. Rapid convergence is ensured for piecewise complex analytic integrals by use of the Petras algorithm, which combines adaptive bisection with adaptive Gaussian quadrature where error bounds are determined via complex magnitudes without evaluating derivatives. The code is general, easy to use, and efficient, often outperforming existing non-rigorous software.

We report on enumerating the triangulations of cyclic polytopes with the new software MPTOPCOM. This is relevant for its connection with higher Stasheff–Tamari orders, which occur in category theory and algebraic combinatorics.

Principal component analysis is one of the most popular unsupervised learning methods for reducing the dimension of a given data set in a high-dimensional Euclidean space. However, computing principal components on a space of phylogenetic trees with fixed labels of leaves is a challenging task since a space of phylogenetic tree is not Euclidean. In 2017, Yoshida et al. defined a notion of tropical principal component analysis and they have applied it to a space of phylogenetic trees. The challenge, however, they encountered was a computational times.In this paper we estimate tropical principal components in a space of phylogenetic trees using the Metropolis-Hasting algorithm. We have implemented an R software package to efficiently estimate tropical principal components and then we have applied it to African coelacanth genomes data set.

In any classroom, different groups of students may have unequal voices. This “lack of democracy” may be particularly problematic in STEM fields. To promote a more inclusive classroom, we developed and tested an online, real-time communication tool: the Mathematics Classroom Collaborator ($$MC^2$$MC2). $$MC^2$$MC2 makes the entry of mathematics easy and intuitive, it includes an option for anonymity, and it works on a variety of platforms, including smart phones, tablets, and notebook computers. In this paper, we share our experience with employing $$MC^2$$MC2 in a statistics service course and an introductory probability course. We describe how this tool creates new communication models for the technologically-enhanced class — models that may help overcome social barriers to create a more inclusive environment, and that may lead to further democratization of learning, including increased participation by women and/or English-language learners. The results of an experiment to measure the effectiveness of $$MC^2$$MC2 compared to Microsoft Word Equation for novice users are also presented.

In most fields, computational models and data analysis have become a significant part of how research is performed, in addition to the more traditional theory and experiment. Mathematics is no exception to this trend. While the system of publication and credit for theory and experiment (journals and books, often monographs) has developed and has become an expected part of the culture, how research is shared and how candidates for hiring, promotion are evaluated, software (and data) do not have the same history. A group working as part of the FORCE11 community developed a set of principles for software citation that fit software into the journal citation system, allow software to be published and then cited, and there are now over 50,000 DOIs that have been issued for software. However, some challenges remain, including: promoting the idea of software citation to developers and users; collaborating with publishers to ensure that systems collect and retain required metadata; ensuring that the rest of the scholarly infrastructure, particularly indexing sites, include software; working with communities so that software efforts “count”; and understanding how best to cite software that has not been published.

Mathematical user interfaces for authoring, collaboration, problem-solving and reasoning invariably rely on the ability to read, write and manipulate complex mathematical expressions. However, very little research has been done on how people read mathematical expressions, let alone how they are understood by the mind. One technique which researchers use to gain insight into how people read and comprehend symbols and complex phenomena are studies using eye-tracking hardware: focus on, and tracking of, pupils in order to determine the reader’s attention and fixation. In this paper we will explore the results of a study on two classes of students: mathematically “expert” (mathematical sciences students) and non-expert (Faculty of Science majors from outside the mathematical sciences). Each participant was presented with a series of mathematical problems (stimuli) and their eyes and attention/focus tracked as they worked through the problems mentally. We will discuss the differences in the two classes, both with respect to the correctness of responses to the problems and the structure of the scanning and identification of important components within the problem. This study has applications in mathematical software usability, accessibility, and design of interfaces, as comprehension of mathematical notation and formalism is assumed in the implementation of the modified symbolism inherent in structured mathematical software interfaces.

The problem is to identify a movable object that is in some sense known, if it is encountered later. Suppose we have a sensor, on a fixed radar station or a moving platform. We have an object, say object A, previously measured, with certain distinct identifiable points $$p_i.$$pi. We know the distances between these points. We later encounter a similar object B and want to know if it is A. We have a sensor that sends and receives electronic signals, and so we measure the distances $$t_i$$ti from the sensor to the distinguished points on B.We first consider the two-dimensional case. Assume there are three distinct points on A. We have our measured distances $$t_1, t_2, t_3$$t1,t2,t3 and previously known distances between the points on A, $$d_1, d_2, d_3$$d1,d2,d3. We derive a polynomial system relating these quantities and show that it is easy to solve yielding a resultant that is the “signature” for A. Its use will eliminate B if B is not A.The generalization to three dimensions is immediate. We need a fourth point. The polynomial system contains many parameters, but we solve it symbolically. We then discuss generalizations involving flexibility. In those cases we need five points and the systems are much more complex.We compare solutions on Magma, Maple, and Fermat computer algebra systems.

A fundamental problem in computer graphics and computer aided design is to convert between a parameterization of a surface and an implicit representation of it. Almost as fundamental is to derive a parameterization for the intersection of two surfaces.In these problems, it seems that resultants, specifically the Dixon resultant, have been underappreciated. Indeed, several well known papers from ten to twenty years ago reported unsuitability of resultant techniques. To the contrary, we show that the Dixon resultant is an extremely effective and efficient method to compute an implicit representation.To use resultants to compute a parameterization of an intersection, we introduce the concept of an “implicit parameterization.” Unlike the conventional parameterization of a curve where x, y, and z are each explicitly given as functions of, say, t, we have three implicit functions, one each for (x, t), (y, t), and (z, t). This concept has rarely been mentioned before. We show that given a (conventional) parameterization for one surface and either an implicit equation for the second, or a parameterization for it, it is straightforward to compute an implicit parameterization for the intersection. Doing so is very easy for the Dixon resultant, but can be very daunting even for well respected Gröbner bases programs.Further, we demonstrate that such implicit parameterizations are useful. We use builtin 3D plotting utilities of a computer algebra system to graph the intersection using our implicit parameterization. We do this for examples that are more complex than the quadric examples usually discussed in intersection papers.

In indoor and outdoor navigation, finding the local position of a sphere in mapping space employing a laser scanning technique with low-cost sensors is a very challenging and daunting task. In this contribution, we illustrate how Gröbner basis techniques can be used to solve polynomial equations arising when algebraic and geometric measures for the error are used. The effectiveness of the suggested method is demonstrated, thanks to standard CAS software like Mathematica, using numerical examples of the real world.

We describe the design and relationships of several Macaulay2 packages that use numerical polynomial homotopy continuation as their engine. Macaulay2 is a computer algebra system built around the classical symbolic computation tools such as Gröbner bases. However, recent Macaulay2 versions include its own fast implementation of homotopy continuation, interfaces to external numerical algebraic geometry software (Bertini and PHCpack), and a unified data structures design that allows the use of the internal and external capabilities interchangeably. The resulting numerical and hybrid tools are of general interest to Macaulay2 users interested in computational experimentation.

Systems of polynomial or algebraic equations with finitely many solutions arise in many areas of applied mathematics. I will discuss the design and implementation of a hybrid symbolic-numeric method based on the endomorphism matrix approach pioneered by Stetter and others. It makes use of numeric Gröbner bases and arbitrary-precision eigensystem computations. I will describe how to assess accuracy, find and remove parasite solutions in the case of fractional degrees in the system, handle multiplicity, as well as some of the other finer points not usually covered in the literature. This work is one of the methods used in the Wolfram Language NSolve function.

The Andrews-Curtis conjecture (ACC) remains one of the outstanding open problems in combinatorial group theory. In short, it states that every balanced presentation of the trivial group can be transformed into a trivial presentation by a sequence of simple transformations. It is generally believed that the conjecture may be false and there are several series of potential counterexamples for which required simplifications are not known. Finding simplifications poses a challenge for any computational approach - the search space is unbounded and the lower bound on the length of simplification sequences is known to be at least superexponential. Various specialised search algorithms have been used to eliminate some of the potential counterexamples. In this paper we present an alternative approach based on automated reasoning. We formulate a term rewriting system ACT for AC-transformations, and its translation(s) into the first-order logic. The problem of finding AC-simplifications is reduced to the problem of proving first-order formulae, which is then tackled by the available automated theorem provers. We report on the experiments demonstrating the efficiency of the proposed method by finding required simplifications for several new open cases.

Data visualization and interaction with large data sets is known to be essential and critical in many businesses today, and the same applies to research and teaching, in this case, when exploring large and complex mathematical objects. GAP is a computer algebra system for computational discrete algebra with an emphasis on computational group theory. The existing XGAP package for GAP works exclusively on the X Window System. It lacks abstraction between its mathematical and graphical cores, making it difficult to extend, maintain, or port. In this paper, we present Francy, a graphical semantics package for GAP. Francy is responsible for creating a representational structure that can be rendered using many GUI frameworks independent from any particular programming language or operating system. Building on this, we use state of the art web technologies that take advantage of an improved REPL environment, which is currently under development for GAP. The integration of this project with Jupyter provides a rich graphical environment full of features enhancing the usability and accessibility of GAP.

Our goal is to develop a high-performance code for factoring a multivariate polynomial in n variables with integer coefficients which is polynomial time in the sparse case and efficient in the dense case. Maple, Magma, Macsyma, Singular and Mathematica all implement Wang’s multivariate Hensel lifting, which, for sparse polynomials, can be exponential in n. Wang’s algorithm is also highly sequential.In this work we reorganize multivariate Hensel lifting to facilitate a high-performance parallel implementation. We identify multivariate polynomial evaluation and bivariate Hensel lifting as two core components. We have also developed a library of algorithms for polynomial arithmetic which allow us to assign each core an independent task with all the memory it needs in advance so that memory management is eliminated and all important operations operate on dense arrays of 64 bit integers. We have implemented our algorithm and library using Cilk C for the case of two monic factors. We discuss details of the implementation and present experimental timing results.

We consider the use of Quantifier Elimination (QE) technology for automated reasoning in economics. There is a great body of work considering QE applications in science and engineering but we demonstrate here that it also has use in the social sciences. We explain how many suggested theorems in economics could either be proven, or even have their hypotheses shown to be inconsistent, automatically via QE.However, economists who this technology could benefit are usually unfamiliar with QE, and the use of mathematical software generally. This motivated the development of a Mathematica Package TheoryGuru, whose purpose is to lower the costs of applying QE to economics. We describe the package’s functionality and give examples of its use.

CindyJS is a system which enables researchers and learners to interactively handle mathematical models on browsers. Though the enhancement of mathematical user interfaces is widely anticipated and promoted so that mathematical models can be handled via familiar web and mobile devices, it seems that the resulting realities and benefits have not yet been fully investigated. In particular, for educational use, more precise knowledge about them will likely help maximize the effect of using newly developed systems. This research is mainly concerned with the comparison between individual use and group use of CindyJS content on tablets. It can be assumed that, in the case of group use, communication between members would give some influence on the strategy of their handling of mathematical models. To investigate how members of a group influence each other’s handling of mathematical models when using CindyJS, we tracked some characteristic quantities from the recorded processes of users’ operations. Through statistical analysis (approximation with finite mixture of beta distributions) of the quantities derived from the cases of individual use and group use respectively, it can be shown that the difference between these two cases is visualized and the above mentioned influence is illustrated.

In this paper, we introduce a novel dynamic mathematics system called NetPad for teaching and learning mathematics in elementary and secondary school. NetPad is a product of Internet Plus Education and can be launched directly from the internet using a web browser. It combines the Internet with dynamic geometry, computer algebra, and automated reasoning technology. NetPad distinguishes itself from other dynamic geometry systems by being an open, internet-based and sharing oriented intelligent system. NetPad is not only a tool but also a cloud platform for creating and sharing. Since NetPad is developed in HTML5, it is platform independent, runs on every operating system and intelligent device, and can be seamlessly integrated into other websites, PowerPoint and other software. The resources of NetPad can be shared to various social networks directly. The functions of NetPad include dynamic geometry drawing, symbolic computation, programming, automated reasoning in geometry, and so on. NetPad was published in March, 2016. Nowadays, there are more than 100,000 users and 30,000 mathematical resources on the NetPad website.

A common computational problem is to compute topological information about a real surface defined by a system of polynomial equations. Our software, called polyTop, leverages numerical algebraic geometry computations from Bertini and Bertini_real with topological computations in javaPlex to compute the Euler characteristic, genus, Betti numbers, and generators of the fundamental group of a smooth real surface. Several examples are used to demonstrate this new software.

Macpherson defined Chern-Schwartz-Macpherson classes by introducing the (local) Euler obstruction function, which is an integer valued function on the variety that is constant on each stratum of a Whitney stratification. By understanding the Euler obstruction, one gains insights about a singular algebraic variety. It was recently shown by the author and B. Wang, how to compute these functions using maximum likelihood degrees. This paper discusses a symbolic and a numerical implementation of algorithms to compute the Euler obstruction at a point.

IntegerSequences is a Mathematica package for computing with integer sequences. Its support for k-regular sequences includes basic closure properties, guessing recurrences, and computing automata. Recent applications have included establishing the structure of extremal a / b-power-free words, obtaining a product formula for the generating function enumerating binomial coefficients by their p-adic valuations, and proving congruences for combinatorial sequences modulo prime powers.

When implementing functionality which requires sparse matrices, there are numerous storage formats to choose from, each with advantages and disadvantages. To achieve good performance, several formats may need to be used in one program, requiring explicit selection and conversion between the formats. This can be both tedious and error-prone, especially for non-expert users. Motivated by this issue, we present a user-friendly sparse matrix class for the C++ language, with a high-level application programming interface deliberately similar to the widely used MATLAB language. The class internally uses two main approaches to achieve efficient execution: (i) a hybrid storage framework, which automatically and seamlessly switches between three underlying storage formats (compressed sparse column, coordinate list, Red-Black tree) depending on which format is best suited for specific operations, and (ii) template-based meta-programming to automatically detect and optimise execution of common expression patterns. To facilitate relatively quick conversion of research code into production environments, the class and its associated functions provide a suite of essential sparse linear algebra functionality (eg., arithmetic operations, submatrix manipulation) as well as high-level functions for sparse eigendecompositions and linear equation solvers. The latter are achieved by providing easy-to-use abstractions of the low-level ARPACK and SuperLU libraries. The source code is open and provided under the permissive Apache 2.0 license, allowing unencumbered use in commercial products.

E-learning systems for mathematics, such as STACK, Maple T.A., and MATH ON WEB that are able to assess answers using mathematical expressions, have been used for mathematics education at universities. The means for inputting mathematical expressions using current interfaces in these mathematics e-Learning systems are cumbersome not only for students entering their answers, but also for teachers authoring educational materials. In most editing software, teachers need to enter mathematical expressions according to LaTeX-style or computer algebra system-style. This exerts a heavy toll on teachers who have never used these systems. For general use of these systems, it is important to improve the means for entering mathematical expressions. In this study, we developed an intelligent editor for authoring educational materials in mathematics e-Learning systems by implementing a mathematical input interface, named MathTOUCH. This interface allows users to enter the desired mathematical expressions through predictive conversion that converts obscure linear strings presented in a colloquial-style into suitable formats. The results of our previous investigation show that MathTOUCH allows higher level of performance than the standard interfaces. Therefore, the proposed editor is expected to overcome the problem of inputting mathematical expressions in e-learning systems for mathematics education.

In 1994, Tillich and Zémor proposed a scheme for a family of hash functions. In the scheme, they used products of $$2 \times 2$$2×2 matrices in special linear group over a field. Since then, other hash functions based on the Tillich and Zémor’s design have been proposed. These cryptographic hash functions are called Cayley hash functions because of the correspondence between their constructions and Cayley graphs of (semi)groups. Most instances of Cayley hash functions have been proved insecure, but the algorithms used to break Cayley hash functions target specific vulnerabilities of each underlying (semi)group used. However, these algorithms don’t seem to invalidate the generic scheme. An overview is presented of some of the latest proposals for Cayley hash functions and related open problems.

Scientific publications are still the most important medium for publishing mathematical research results. They serve as a container for different types of mathematical research data, especially mathematical models, theories, theorems, conjectures, proofs, algorithms, etc. They also link to mathematical software and simulations which has became more and more important for mathematics and applications. Therefore it seems to be natural to use publications for a more sophisticated analysis of mathematical research data, especially software. Mathematical publications are well-structured and use a more or less standard terminology for content, e.g., theorems, proofs, etc, and the formal structure. Nevertheless, publications could be used as a starting point to develop information services for mathematical research data. In the talk, the publication-based approach for mathematical software and a possible extension to mathematical models are discussed.

We present the Julia package HomotopyContinuation.jl, which provides an algorithmic framework for solving polynomial systems by numerical homotopy continuation. We introduce the basic capabilities of the package and demonstrate the software on an illustrative example. We motivate our choice of Julia and how its features allow us to improve upon existing software packages with respect to usability, modularity and performance. Furthermore, we compare the performance of HomotopyContinuation.jl to the existing packages Bertini and PHCpack.

This paper gives a brief overview of Tarski, a system for computing with Tarski formulas, which are boolean combinations of non-linear polynomial constraints over the reals. It gives an overview of Tarski’s basic functionality, then goes into more detail on facilities Tarski provides for checking the satisfiability of conjunctions of constraints that are able to produce “unsat cores” for unsatisfiable inputs.

Fully homomophic encryption enables private computation over sensitive data, such as medical data, via potentially quantum-safe primitives. In this extended abstract we provide an overview of an implementation of a private-key fully homomorphic encryption scheme in a protocol for private Naive Bayes classification. This protocol allows a data owner to privately classify her data point without direct access to the learned model. We implement this protocol by performing privacy-preserving classification of breast cancer data as benign or malignant.

We study functions of the roots of a univariate polynomial of degree $$n\ge 1$$n≥1 in which the roots have a given multiplicity structure $${\varvec{\mu }}$$μ, denoted by a partition of n. For this purpose, we introduce a theory of $${\varvec{\mu }}$$μ-symmetric polynomials which generalizes the classic theory of symmetric polynomials. We designed three algorithms for checking if a given root function is $${\varvec{\mu }}$$μ-symmetric: one based on Gröbner bases, another based on preprocessing and reduction, and the third based on solving linear equations. Experiments show that the latter two algorithms are significantly faster. We were originally motivated by a conjecture about the $${\varvec{\mu }}$$μ-symmetry of a certain root function $$D^+({\varvec{\mu }})$$D+(μ) called D-plus. This conjecture is proved to be true. But prior to the proof, we studied the conjecture experimentally using our algorithms.

In the past four years, the author has developed more than 120 video lectures for a linear algebra course, each of which is of about 10 min duration, and has tried to conduct flipped class. The author set tasks for the students using Moodle (LMS) questions, which are mainly of STACK type, in order to check if they have really studied the video materials and how deeply they understand them. According to the questionnaire result, in the case that the questions have too many input fields or require some CAS-formatted texts, the students may have some difficulty to answer the questions, especially with mobile phones. Multiple choice type or true-false questions are very simple to answer with such devices. In the latter half of the last academic year, the author developed CAS programs to automatically generate multiples of 100 mutually different matrices for some problems. For example, one of the programs generates the question data to select diagonalizable matrices from 10 matrices of degree 3. In order to prove that the students actually solved the questions by themselves, they were instructed to submit papers describing the process of the solution. We are planning to develop more generating programs to cover the entire course, including non-computational tasks.

An innovative approach is proposed in designing intuitive interfaces for solving systems of linear and nonlinear equations over Cartesian products of general vector spaces. The interfaces enable scientific computing practitioners and learners to enter equations in WYSIWYG manner, lets the software generate vector representations of equations/variables internally and outputs the solutions in the desired forms automatically. Such interfaces save more time than algorithmic improvement for one-time users and students.