Results 2261 - 2270 of 23900

Abstract not available.

It is very tempting, as a mathematician, to use Lean to try and check some of your own proofs, especially when you're unsure of them. The obvious problem with that is that no paper proof is as detailed as a formalized proof, but this is not the only pitfall. I will talk about some of the other problems one might encounter.

Bit-precise reasoning in the context of Satisfiability Modulo Theories (SMT) is a key requirement for many formal methods applications, both in industry and academia. Efficiently reasoning about bit-vector constraints in SMT has been an ongoing challenge for many years. Existing approaches all struggle with scalability for increasing bit widths, especially in the presence of arithmetic operators. The dominant state-of-the-art approach for bit-vector reasoning is bit-blasting, an eager reduction to propositional logic, which is combined with aggressive simplifications of the input constraints prior to the actual reduction step. And even though bit-blasting may come at the cost of significantly increasing the formula size, which is the main reason for scalability issues with this technique, it is surprisingly efficient in practice---thanks to state-of-the-art SAT solvers. This talk will explore the main challenges for bit-vector reasoning and highlight state-of-the-art techniques. In particular, we will present a recent procedure that aims at improving the scalability of bit-blasting.

Abstract not available.

As Thurston describes in his famous essay "On proof and progress in mathematics," the answer to the question "What is it that mathematicians accomplish?" is multifaceted. Inspired by Turing's "Computing machinery and intelligence," we propose a series of tests to help identify whether a generative AI system can meaningfully contribute to the process of doing mathematics.

Walnut is free software that can rigorously prove or disprove a variety of claims in number theory, combinatorics, and theoretical computer science, merely by stating the claim in an extension of Presburger arithmetic called Buchi arithmetic. (It is not a general-purpose proof assistant like Isabelle/HOL, Coq, or Lean.) Although the worst-case running time is truly astronomical, it nevertheless has still been used in over 100 books and articles to reprove existing results, correct false claims in the literature, resolve previously-unproved conjectures, and prove new results. In my talk I will demonstrate some of its capabilities and invite suggestions about how it might be integrated with existing proof assistants and theorem provers.

Walnut is available at https://cs.uwaterloo.ca/~shallit/walnut.html .