Thread
Stories related to "Solving (Some) Formal Math Olympiad Problems" across the full archive.
Key quote from abstract: "...we implement a new system, Certigrad, for optimizing over stochastic computation graphs, and we generate a formal (i.e. machine-checkable) proof that the gradients sampled by the system are unbiased estimates of the true mathematical gradients. We train a variational aut...
Tackling the Problems of Philosophy with Ideas from Mathematics, Economics, and Physics
(thebigquestions.com)
This large-scale research project (with european funding) might make proof assistants, and in particular Isabelle/HOL, more usable for mathematicians. The [project plan](https://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/DoA.pdf) contains many more details on the expected course of actions. This effor...
Automatically Proving Mathematical Theorems with Evolutionary Algorithms and Proof Assistants (2016)
(arxiv.org)
Trimmed abstract: " Evolutionary algorithms, known to be flexible and versatile, have been successfully applied to handle a variety of scientific and engineering problems in numerous disciplines for also several decades... In the article, we describe in detail our first, ad-hoc attempt to [use them ...
Abstract: "Industry standard implementations of math.h claim (often without formal proof) tight bounds on floatingpoint errors. We demonstrate a novel static analysis that proves these bounds and verifies the correctness of these implementations. Our key insight is a reduction of this verification t...
(This paper is from the First Workshop on Formal Methods in Software Engineering Education and Training in 2015)
From the abstract (yes, I'm abstracting the abstract, because it actually is too long!):
"[Formal Methods] plays just a minor role in both the everyday work of software engineers as...
This is a talk by Prof Kevin Buzzard given at Microsoft Research recently. In it, he proposes a program for formalizing the undergraduate mathematics curriculum in Lean. I personally found it fascinating, partly because this goal resonates strongly with me, but also because of the cultural and socio...
> As the usage of theorem prover technology expands, so too does the reliance on correctness of the tools. Metamath Zero is a verification system that aims for simplicity of logic and implementation, without compromising on efficiency of verification. It is formally specified in its own language, an...