We present a simple programming language based on Gödel numbering and prime
factorization, enhanced with explicit, scoped loops, allowing for easy program
composition. Further, we will present a theorem prover that allows expressing
and working with formal systems. The theorem prover is simple as it relies
merely on a substitution rule and set equality to derive theorems. Finally, we
will represent the programming language in the theorem prover. We will show the
syntax and semantics of both, and then provide a few example programs and their
evaluation.

基于哥德尔编号和质因数分解的简单编程语言，配合具有显式作用域的循环和定理证明器，可以表示和工作于形式系统。编程语言和定理证明器之间可以相互表示，并提供实例程序和它们的求值。

Budge：一种编程语言和定理证明器

Budge: a programming language and a theorem prover

Prime factorization is a difficult problem with classical computing, whose
exponential hardness is the foundation of Rivest-Shamir-Adleman (RSA)
cryptography. With programmable quantum devices, adiabatic quantum computing
has been proposed as a plausible approach to solve prime factorization, having
promising advantage over classical computing. Here, we find there are certain
hard instances that are consistently intractable for both classical simulated
annealing and un-configured adiabatic quantum computing (AQC). Aiming at an
automated architecture for optimal configuration of quantum adiabatic
factorization, we apply a deep reinforcement learning (RL) method to configure
the AQC algorithm. By setting the success probability of the worst-case problem
instances as the reward to RL, we show the AQC performance on the hard
instances is dramatically improved by RL configuration. The success probability
also becomes more evenly distributed over different problem instances, meaning
the configured AQC is more stable as compared to the un-configured case.
Through a technique of transfer learning, we find prominent evidence that the
framework of AQC configuration is scalable -- the configured AQC as trained on
five qubits remains working efficiently on nine qubits with a minimal amount of
additional training cost.

采用一种深度强化学习（RL）方法配置自适应量子因子分解算法，该算法的效果得到了显著提高，概率分布更加均匀，具有可扩展性，最小化了额外的训练成本。

量子绝热质因数分解问题的难实例学习

Hard instance learning for quantum adiabatic prime factorization

We investigate prime factorization from two perspectives: quantum annealing
and computational algebraic geometry, specifically Gr\"obner bases. We present
a novel scalable algorithm which combines the two approaches and leads to the
factorization of all bi-primes up to just over $200 \, 000$, the largest number
factored to date using a quantum processor.

研究了量子退火和计算代数几何 (特别是 Gröbner 基) 两种方法在质因数分解中的应用。我们提出了一种新的可扩展算法，结合了两种方法，成功地分解了所有双质数直到刚刚超过 200,000，这是迄今为止使用量子处理器分解的最大数字。