14:08 <infinisil> Proofs!

14:09 <MichaelRaskin> simpson: actually there is a lot of interesting work in auto-generating proofs

14:10 <MichaelRaskin> It is quite interesting to see how top systems at CASC progress at, first-order logic proof search

14:12 <simpson> It's definitely interesting.

14:12 <MichaelRaskin> Pure FOL has the benefit of multiple checkers available, so one could _hope_ to escape the everpresent «is this a buggy optimisation in Coq?»

14:12 <MichaelRaskin> With SMT you already need to believe the complicated stuff to be correct

14:13 <MichaelRaskin> It looks like higher-order high-powered logics are attractive for the first steps, because they give you basic structures for free; I don't know any published prover-friendly encodings of a large enough set theory into pure FOF

14:14 <MichaelRaskin> I like FOF because there is completeness theorem for it…

14:15 <simpson> I have been working with the formalism in https://arxiv.org/abs/1706.00526

14:15 <MichaelRaskin> I tried to do semi-automated proof-completion with FOF provers (me: provide axioms, claims, and lemmas; automated prover: prove implications)

14:15 <MichaelRaskin> It seems fine, but a library of basic definitions is missing, and I don't like what I got with my first attempts

14:16 <simpson> Which corresponds to regular logic. It also neatly corresponds to a fragment of Lojban which is powerful enough to state things like "Given that all cats have a cat species, and all animals have an animal species, and all cats are animals, and all cat species are animal species, anything which is a cat with a cat species is also an animal with an animal species."

14:16 <simpson> I like Lojban's free basic definitions. They are somewhat tautological, but a Lojban-English dictionary can give them 'meaning'

14:20 <MichaelRaskin> I want to have a clear path to translate probability theory as a list of assumptions (without modifying the core), so I would like to have basic FOF and a reasonably close to standard set theory there.

14:21 <simpson> Interesting. I've played a bit with sheaves and Bayesian nets, which are a little limited causally but still might be useful.

14:22 <MichaelRaskin> I don't want to cut off central limit theorem, and I don't want to hard code it into the core and pray for correctness, and I definitely do not want to prove it from scratch without being able to translate the proof from a random textbook

14:23 <simpson> Mm.

14:24 <MichaelRaskin> That implies I want a sane translation of ZFC.

14:24 <MichaelRaskin> I have a workflow for lemma-hopping that seems OK, one day I will try again.