-
Prove-It: A Proof Assistant for Organizing and Verifying General Mathematical Knowledge
Authors:
Wayne M. Witzel,
Warren D. Craft,
Robert D. Carr,
Joaquín E. Madrid Larrañaga
Abstract:
We introduce Prove-It, a Python-based general-purpose interactive theorem-proving assistant designed with the goal of making formal theorem proving as easy and natural as informal theorem proving (with moderate training). Prove-It uses a highly-flexible Jupyter notebook-based user interface that documents interactions and proof steps using LaTeX. We review Prove-It's highly expressive representati…
▽ More
We introduce Prove-It, a Python-based general-purpose interactive theorem-proving assistant designed with the goal of making formal theorem proving as easy and natural as informal theorem proving (with moderate training). Prove-It uses a highly-flexible Jupyter notebook-based user interface that documents interactions and proof steps using LaTeX. We review Prove-It's highly expressive representation of expressions, judgments, theorems, and proofs; demonstrate the system by constructing a traditional proof-by-contradiction that $\sqrt{2}\notin\mathbb{Q}$; and discuss how the system avoids inconsistencies such as Russell's and Curry's paradoxes. Extensive documentation is provided in the appendices about core elements of the system. Current development and future work includes promising applications to quantum circuit manipulation and quantum algorithm verification.
△ Less
Submitted 26 December, 2020; v1 submitted 20 December, 2020;
originally announced December 2020.
-
Implications of Electronics Constraints for Solid-State Quantum Error Correction and Quantum Circuit Failure Probability
Authors:
James E. Levy,
Malcolm S. Carroll,
Anand Ganti,
Cynthia A. Phillips,
Andrew J. Landahl,
Thomas M. Gurrieri,
Robert D. Carr,
Harold L. Stalford,
Erik Nielsen
Abstract:
In this paper we present the impact of classical electronics constraints on a solid-state quantum dot logical qubit architecture. Constraints due to routing density, bandwidth allocation, signal timing, and thermally aware placement of classical supporting electronics significantly affect the quantum error correction circuit's error rate. We analyze one level of a quantum error correction circuit…
▽ More
In this paper we present the impact of classical electronics constraints on a solid-state quantum dot logical qubit architecture. Constraints due to routing density, bandwidth allocation, signal timing, and thermally aware placement of classical supporting electronics significantly affect the quantum error correction circuit's error rate. We analyze one level of a quantum error correction circuit using nine data qubits in a Bacon-Shor code configured as a quantum memory. A hypothetical silicon double quantum dot quantum bit (qubit) is used as the fundamental element. A pessimistic estimate of the error probability of the quantum circuit is calculated using the total number of gates and idle time using a provably optimal schedule for the circuit operations obtained with an integer program methodology. The micro-architecture analysis provides insight about the different ways the electronics impact the circuit performance (e.g., extra idle time in the schedule), which can significantly limit the ultimate performance of any quantum circuit and therefore is a critical foundation for any future larger scale architecture analysis.
△ Less
Submitted 3 May, 2011;
originally announced May 2011.
-
The impact of classical electronics constraints on a solid-state logical qubit memory
Authors:
James E. Levy,
Anand Ganti,
Cynthia A. Phillips,
Benjamin R. Hamlet,
Andrew J. Landahl,
Thomas M. Gurrieri,
Robert D. Carr,
Malcolm S. Carroll
Abstract:
We describe a fault-tolerant memory for an error-corrected logical qubit based on silicon double quantum dot physical qubits. Our design accounts for constraints imposed by supporting classical electronics. A significant consequence of the constraints is to add error-prone idle steps for the physical qubits. Even using a schedule with provably minimum idle time, for our noise model and choice of…
▽ More
We describe a fault-tolerant memory for an error-corrected logical qubit based on silicon double quantum dot physical qubits. Our design accounts for constraints imposed by supporting classical electronics. A significant consequence of the constraints is to add error-prone idle steps for the physical qubits. Even using a schedule with provably minimum idle time, for our noise model and choice of error-correction code, we find that these additional idles negate any benefits of error correction. Using additional qubit operations, we can greatly suppress idle-induced errors, making error correction beneficial, provided the qubit operations achieve an error rate less than $2 \times 10^{-5}$. We discuss other consequences of these constraints such as error-correction code choice and physical qubit operation speed. While our analysis is specific to this memory architecture, the methods we develop are general enough to apply to other architectures as well.
△ Less
Submitted 31 March, 2009;
originally announced April 2009.
