Formal verification of upper bounds on translative packing densities

Packing problems are concerned with filling the space with copies of a certain object, so that the least amount of space stays unoccupied. The famous Kepler conjecture asserts that the cannonball packing of spheres is the most efficient packing achievable, and was recently formally proven by Hales.<br/><br/>Dostert, Guzman, Oliveira Filho and...

Axiomatic Projective Geometry

Starting with the three axioms of projective geometry, this paper explores concepts such as perspectives, projective maps, and harmonic additions that are unique to this geometry. In addition, important theorems such as Pappus's Theorem, Desargue's Theorem, and the Fundamental Property are mentioned and worked with extensively.

De wortelsystemen in E8

In dit verslag wordt besproken hoe je deelwortelsystemen in het wortelsysteem E8 kan vinden. In het begin wordt er algemene theorie over wortelsystemen gegeven. Vervolgens worden er twee manieren besproken hoe je deelwortelsystemen in wortelsystemen kan vinden. Uiteindelijk worden de twee manieren toegepast op E8 om deelwortelsystemen in E8 te...

Stabiliteit van de fiets

In dit project is onderzoek gedaan naar de stabiliteit van de fiets. Hiervoor is het model gebruikt van een fiets van Herfkens. In dit model kan de berijder niet sturen en zit vast verbonden aan de fiets. Dit model bestaat uit 25 parameters. De stabiliteit is onderzocht aan de hand van de stuurhoek en de kanteling van de fiets. Er is gekeken...

Computing Measures for Tree-Basedness of Phylogenetic Networks

Phylogenetic networks are a type of directed acyclic graph used to represent evolutionary relationships that contain events such as hybridization or horizontal gene transfer. When a network<br/>lacks such events it is a phylogenetic tree. Some phylogenetic networks that are not trees can<br/>however be represented as a tree with additional...

The Borsuk-Ulam Theorem in Combinatorics

We examine and prove the Borsuk-Ulam theorem and its combinatorial equivalent Fan's lemma. The theory of simplicial complexes and triangulations plays an important role in this. The Borsuk-Ulam theorem and Fan's lemma will be used to provide proofs for the Brouwer fixed point theorem and the combinatorial Sperner's lemma. Lastly the Borsuk-Ulam...

A study of the 1984 report An Automatic Proof Procedure For Several Geometries by Th. Bruyn and H.L. Claasen

This report is a discussion of the 1984 report 'An automatic proof procedure for several geometries' by Th. Bruyn and H.L. Claasen, inspired by a personal desire to understand the work of Th. Bruyn. See: http://resolver.tudelft.nl/uuid:b768c6ce-f625-4236-9b0b-32a47fab143e <br/>Bruyn and Claasen prove that certain true propositions of the theory...