Engineered nanoscale systems that provide access to the quantum properties of matter are heralding a revolution in physics and technology. Control over single quantum objects, such as a single electron or photon, and over interactions between them provides the means to engineer the correlations that make quantum technologies a revolutionary advance over their current counterparts. An interface between a stationary matter and a flying optical quantum bit (qubit) is a fundamental building block of the inter-connects that will make quantum technologies useful on a large scale. Solid-state devices have shown strongly coupled light-matter interfaces, efficient light collection, and quantum control of coherent matter nodes. Progress on fabrication techniques to enhance spin and optical coherence properties, combined with important theoretical efforts on modelling complex environments, have yielded significant gains in these areas. Indeed, recent demonstrations using optically addressable spins in semiconductors include a loophole-free test of Bell's inequalities, the generation of photonic states involved in measurement-based quantum computation, and the realisation of quantum internet primitives. Alongside ultracold atoms and superconducting circuits, such optically active solid-state platforms provide developments with distinct long-term advantages due to their ease of integration with combined classical optical and electrical elements. This project will put together a next-generation solid-state quantum networking node that combines the latest developments in the quantum optical research community -- optical device integration, all-optical electron spin control, and nuclear spin coherence and control -- to deliver a platform that outperforms other candidate technologies on the combined metrics of optical coherence and efficiency, quantum bit control, and quantum memory lifetime. This proposal consists of realising this combination by leveraging two recent breakthroughs in a system already known as the best single photon source - III-V semiconductor quantum dots: (1) open optical microcavities as a versatile interface to reach a strong light-matter coupling and high collection efficiency, and (2) strain-free GaAs quantum dots, as host for a coherent matter quantum bit, and on which preliminary measurements indicate a two orders of magnitude improvement in coherence time over the state of the art (InAs quantum dots). As a first major benchmark and the major deliverable of this proposal, a deterministic quantum gate will be performed between two photon qubits, leveraging the optical and spin coherence of this new generation of quantum dots. This proposal aims to reach beyond 1MHz entanglement rate between two photon qubits while achieving a few-percent error rate - a more than four orders of magnitude improvement of the rate-fidelity product over previous attempts in the optical domain. This will serve as a proof-of-concept to establish this platform as the optimal choice for investment towards large-scale arrays of quantum optical devices. Finally, developing this GaAs quantum dot platform promises to equip the leading commercial single-photon emitters with a long-lived nuclear-spin memory, the missing piece for this otherwise exquisite photonics platform. This addition would allow the demonstration of long-lived entanglement across distant quantum nodes, a crucial step en route to a quantum internet where such entanglement can be used as a resource for communication and computation.

Incremental advances in semiconductor technology of the past decades led to unprecedented miniaturization of optoelectronic integrated circuits, which now use billions of transistors, each containing only hundreds of atoms. However, these most sophisticated devices still rely on collective phenomena such as electric currents and light beams. These classical concepts are limited by atomic-scale effects and allow no further progress through miniaturization. Overcoming this bottleneck, would require a new generation of devices where atomic scale effects are no longer an obstacle but are used as a resource to build circuits through precise placement of individual atoms while exploiting quantum effects to boost information storage and processing capacity. Recent innovations in semiconductor material science and technology offer new routes to atomic scale miniaturisation. This project relies on a new type of semiconductor quantum dots, which are tiny semiconductor crystals consisting of only a few thousand atoms. A comprehensive program of material development and experimental physics studies will seek to demonstrate quantum information storage and processing with nuclear magnetic states of individual atoms incorporated into a quantum dot. The broad goal of this proposal is to understand fundamental phenomena and develop material technologies that will stimulate and guide the transition from existing classical digital chips to future devices, which will eventually use every individual atom of a semiconductor crystal as a resource to build integrated circuits with Avogadro-scale number of elementary units and unprecedented information processing power and energy efficiency.

This research applies methods and tools from mathematical knowledge management and theorem proving to theoretical economics, by working with a class of cooperative games called pillage games. Pillage games, introduced by Jordan in 2006, provide a formal way of thinking about the ability of powerful coalitions to take resources from less powerful ones. While their name suggests primitive, violent interactions, pillage games are more applicable to advanced democracies, in which coalitions seek to form governments to alter the distribution of society's resources in their favour. If, for some allocation of society's resources, the coalition preferring another allocation is stronger than that preferring the status quo, the other allocation `dominates' the status quo. The most conceptually intriguing, and the most computationally intractable solution concept for cooperative games is the `stable set'. A stable set, has two features: no allocation in the set dominates another; each allocation outside the set is dominated by an allocation in the set. For pillage games with three agents under a few additional conditions, we have determined when stable sets exist, that they are unique and contain no more than 15 allocations, and how to determine them for a given power function. In this research, we first formally represent the mathematical knowledge developed in Jordan's and our work using sTeX, a mathematical knowledge management tool. This allows, e.g., automatic identification of how various results depend on each other. We then use two modern automated theorem provers (ATPs), Isabelle and Theorema, to formally prove these results. Theorem proving is a hard task and if not provided with domain specific knowledge ATPs have to search through big search spaces in order to find proofs. To increase their reasoning power, we shall seek to identify recurring patterns in proofs, and extract proof tactics, reducing the interactions necessary to prove the theorems interactively. As important results in pillage games can be summarised in pseudo-algorithms, containing both computational and non-computational steps, we shall study such pseudo-algorithms, seeking to push them towards the much more efficient computational steps. Finally, we shall use the identified proof tactics to help the ATPs prove new results in order evaluate their true value. The research seeks to make a number of contributions. For theorem proving, pillage games form a new set of challenge problems. As the study of pillage games is new, and the canon of applicable knowledge small, this gives an unprecedented opportunity to encode most of it. The research will expand the tractable problem domain for ATPs; and - by identifying successful tactics - increase both the efficiency with which ATPs search for proofs, and - ideally - their ability to establish new results. For economics, this is the first major application of formal knowledge management and theorem proving techniques. The few previous applications of ATP to economics have formalised isolated results without engaging economists and have thus largely gone unnoticed by the discipline. As cooperative games are a known hard class of economic problems, and pillage games known to be tractable, this research therefore presents a strong `proof of concept' for the use of ATP within economics. Cooperative game theory is formally similar to graph theory, the techniques and insights developed may be applicable to matching problems, network economics, operations research, and combinatorial optimisation more generally. Additionally, the researchers will introduce ATP techniques to the leading PhD summer school in computational economics, and are working in collaboration with economic theorists with strong computational backgrounds. Thus, the research seeks to form a focal point for formal knowledge management and theorem proving efforts in economics.