Searcharxiv⌕ Search

arXiv subjects

Alexei Vernitski

Publications and source records attributed to Alexei Vernitski.

17 recordsLinked to original sources
arXiv2025

Capturing properties of planar diagrams in Lean proof assistant software

Automated proof assistants are a technology pre-empting mistakes in mathematics. In our practice we have seen that reasoning about planar diagrams is difficult to both humans and computers. One example that has led to wrong statements in publications is that an orientation-preserving mapping is not always defined by how it acts on triples of elements. In this paper we formalise orientation-preserving mappings in proof assistant software Lean and report on our take-aways.

math.CO↗
arXiv2025

Divisibility rules for integers presented as permutations

In this note, we represent integers in a type of factoradic notation. Rather than use the corresponding Lehmer code, we will view integers as permutations. Given a pair of integers n and k, we give a formula for n mod k in terms of the factoradic digits, and use this to deduce various divisibility rules.

math.NT↗
arXiv2024

Gauss diagrams as cubic graphs: The choice of the Hamiltonian cycle matters

We explore to what extent the properties of a Gauss diagram are affected by the choice of its Hamiltonian cycle. We present an example of a realizable Gauss diagram and an unrealizable Gauss diagram that differ only by a choice of the Hamiltonian cycle. We present an example of two Gauss diagrams that correspond to different curves and differ only by a choice of the Hamiltonian cycle. We prove that a certain natural type of change of the Hamiltonian cycle preserves the realizability of the Gauss diagram.

math.GT↗
arXiv2024

Groups of permutations preserving orientation (parity) of subsets of a fixed size, and related monoids

We study permutations on n elements preserving orientation (parity) of every subset of size k. We describe all groups of these permutations. Unexpectedly, these groups (except for some special cases) are either trivial, cyclic or dihedral. In this context, we define and study monoids generalizing monoids of order-preserving mappings and monoids of orientation-preserving mappings.

math.CO↗
arXiv2023

Automated reasoning for proving non-orderability of groups

We demonstrate how a generic automated theorem prover can be applied to establish the non-orderability of groups. Our approach incorporates various tools such as positive cones, torsions, generalised torsions and cofinal elements.

math.GT↗
arXiv2023

Machine learning discovers invariants of braids and flat braids

We use machine learning to classify examples of braids (or flat braids) as trivial or non-trivial. Our ML takes form of supervised learning using neural networks (multilayer perceptrons). When they achieve good results in classification, we are able to interpret their structure as mathematical conjectures and then prove these conjectures as theorems. As a result, we find new convenient invariants of braids, including a complete invariant of flat braids.

math.GT↗
arXiv2022

Describing realizable Gauss diagrams using the concepts of parity or bipartate graphs

Two recent publications describe realizable Gauss diagrams using conditions stating that the number of chords in certain sets of chords is even or odd. We demonstrate that these descriptions are incorrect by finding multiple counter-examples. However, the idea of having a parity-based description of realizable Gauss diagrams is attractive. We recall that realizability of Gauss diagrams as touch curves can be described via bipartite graphs. We show that realizable Gauss diagrams can be described via bipartite graphs.

math.GT↗
arXiv2022

Orientation-preserving and orientation-reversing mappings: a new description

We characterise the respective semigroups of mappings that preserve, or that preserve or reverse orientation of a finite cycle, in terms of their actions on oriented triples and oriented quadruples. This leads to a proof that the latter semigroup coincides with the semigroup of all mappings that preserve intersections of chords on the corresponding circle.

math.CO↗
arXiv2021

A blind spot in undergraduate mathematics: The circular definition of the length of the circle, and how it can be turned into an enlightening example

We highlight the fact that in undergraduate calculus, the number pi is defined via the length of the circle, the length of the circle is defined as a certain value of an inverse trigonometric function, and this value is defined via pi, thus forming a circular definition. We present a way in which this error can be rectified. We explain that this error is instructive and can be used as an enlightening topic for discussing different approaches to mathematics with undergraduate students.

math.HO↗
arXiv2021

Untangling Braids with Multi-agent Q-Learning

We use reinforcement learning to tackle the problem of untangling braids. We experiment with braids with 2 and 3 strands. Two competing players learn to tangle and untangle a braid. We interface the braid untangling problem with the OpenAI Gym environment, a widely used way of connecting agents to reinforcement learning problems. The results provide evidence that the more we train the system, the better the untangling player gets at untangling braids. At the same time, our tangling player produces good examples of tangled braids.

cs.LG↗
arXiv2021

Circle graphs (chord interlacement graphs) of Gauss diagrams: Descriptions of realizable Gauss diagrams, algorithms, enumeration

Chord diagrams, under the name of Gauss diagrams, are used in low-dimensional topology as an important tool for studying curves or knots. Those Gauss diagrams that correspond to curves or knots are called realizable. The theme of our paper is the fact that realizability of a Gauss diagram can be expressed via its circle graph. Accordingly, one can define and study realizable circle graphs (with realizability of a circle graph understood as realizability of any one of chord diagrams corresponding to the graph). Several studies contain theorems purporting to prove the fact. We check several of these descriptions experimentally and find counterexamples to the descriptions of realizable Gauss diagrams in some of these publications. We formulate new descriptions of realizable circle graphs and present an elegant algorithm for checking if a circle graph is realizable. We enumerate realizable circle graphs for small sizes and comment on these numbers. Then we concentrate on one type of curves, called meanders, and study the circle graphs of their Gauss diagrams.

math.GT↗
arXiv2018

Encoding shortest paths in graphs assuming the code is queried using bit-wise comparison

One model of message delivery in a computer network is based on labelling each edge by a subset of a (reasonably small) universal set, and then encoding a path as the union of the labels of its edges. Earlier work suggested using random edge labels, and that approach has a disadvantage of producing errors (false positives). We demonstrate that if we make an assumption about the shape of the network (in this paper we consider networks with a dense core and a tree-like periphery) and assume that messages are delivered along shortest paths, we can label edges in a way which prevents any false positives.

math.CO↗
arXiv2017

Efficient Adaptive Implementation of the Serial Schedule Generation Scheme using Preprocessing and Bloom Filters

The majority of scheduling metaheuristics use indirect representation of solutions as a way to efficiently explore the search space. Thus, a crucial part of such metaheuristics is a "schedule generation scheme" -- procedure translating the indirect solution representation into a schedule. Schedule generation scheme is used every time a new candidate solution needs to be evaluated. Being relatively slow, it eats up most of the running time of the metaheuristic and, thus, its speed plays significant role in performance of the metaheuristic. Despite its importance, little attention has been paid in the literature to efficient implementation of schedule generation schemes. We give detailed description of serial schedule generation scheme, including new improvements, and propose a new approach for speeding it up, by using Bloom filters. The results are further strengthened by automated control of parameters. Finally, we employ online algorithm selection to dynamically choose which of the two implementations to use. This hybrid approach significantly outperforms conventional implementation on a wide range of instances.

cs.DS↗
arXiv2016

Ranks of ideals in inverse semigroups of difunctional binary relations

The set D_n of all difunctional relations on an n element set is an inverse semigroup under a variation of the usual composition operation. We solve an open problem of Kudryavtseva and Maltcev (2011), which asks: What is the rank (smallest size of a generating set) of D_n? Specifically, we show that the rank of D_n is B(n)+n, where B(n) is the nth Bell number. We also give the rank of an arbitrary ideal of D_n. Although D_n bears many similarities with families such as the full transformation semigroups and symmetric inverse semigroups (all contain the symmetric group and have a chain of J-classes), we note that the fast growth of rank(D_n) as a function of n is a property not shared with these other families.

math.GR↗
arXiv2016

Yes-no Bloom filter: A way of representing sets with fewer false positives

The Bloom filter (BF) is a space efficient randomized data structure particularly suitable to represent a set supporting approximate membership queries. BFs have been extensively used in many applications especially in networking due to their simplicity and flexibility. The performances of BFs mainly depends on query overhead, space requirements and false positives. The aim of this paper is to focus on false positives. Inspired by the recent application of the BF in a novel multicast forwarding fabric for information centric networks, this paper proposes the yes-no BF, a new way of representing a set, based on the BF, but with significantly lower false positives and no false negatives. Although it requires slightly more processing at the stage of its formation, it offers the same processing requirements for membership queries as the BF. After introducing the yes-no BF, we show through simulations, that it has better false positive performance than the BF.

cs.DS↗