Login
You're viewing the discuss.systems public feed.
  • calx u-latorcalx@infosec.exchange
    Jul 29, 2026, 2:07 PM

    @mario @0xabad1dea @david_chisnall i can't seem to agree with this take, i am probably super wrong, but

    i'll define a theorem prover as something that, when provided with a proof, can say with 100% surety whether the proof contains any mistake or not, and thus if it is valid, according to current database of proven methods

    and if you agree with my definition, that should also include anything that isn't directly a part of the theorem prover, but still impact how it's output gets interpreted by the human, including,
    - the software,
    - the formal proof for that software,
    - the hardware,
    - the formal proof for that hardware,
    - the model of the hardware, and
    - even the human brain interpreting the results,

    without having a 100% surety on all these terms, we can't say that, when theorem prover verifies a proof, the proof is true, with 100% surety.

    💬 1🔄 0⭐ 1

Replies

  • Mariomario@don.tbully.me
    Jul 29, 2026, 2:16 PM
    @calx @0xabad1dea @david_chisnall a proof is only valid within it's system. in the case of rocq the system is the calculus of inductive constructions i.e.
    there are extraction systems which translate the formal language of rocq (gallina) into high-level code like ocaml or c.
    these are two different structures, like you have the formal logic side and you have the computation side which are connected via the curry howard correspondence.
    like a theorem prover assists you by providing tools for theorem proving, it's scope is formal logic.
    💬 1🔄 0⭐ 0
  • calx u-latorcalx@infosec.exchange
    Jul 29, 2026, 3:22 PM

    @mario @0xabad1dea @david_chisnall this kinda is making sense to me
    basically, what i think you mean is

    when we say "this proof is verified by xyz verifier", all the uncertainty that i mention gets put under the assumption that verifier isn't faulty

    right?

    i was going over whether that assumption can be true in my post, and what you're saying is once we add that assumption to our system, the proof becomes valid in that system, right?

    💬 1🔄 0⭐ 0
  • Mariomario@don.tbully.me
    Jul 29, 2026, 3:29 PM
    @calx @0xabad1dea @david_chisnall > once we add that assumption to our system, the proof becomes valid in that system, right?
    if you are able to prove that assumption within your knowledge space and tactics then it already was part of the system in the first place. but now you don't only have proven that assumption in your system but you have also found an instance of the assumption you can then further use in proving more stuff. at least for constructive logic thats the case.

    > the assumption that verifier isn't faulty
    that can be proven actually
    💬 1🔄 0⭐ 0
  • calx u-latorcalx@infosec.exchange
    Jul 29, 2026, 3:39 PM

    @mario @0xabad1dea @david_chisnall
    > > the assumption that verifier isn't faulty
    > that can be proven actually

    but to remove that assumption and to prove it, you'll need to add some other assumption, maybe about the hardware you'll use to prove the previous assumption, or maybe the model modelling the system on which the theorem prover will run

    in no way can a theorem prover, escape from its dependence on the assumptions about the system it is running on

    a normal proof doesn't have any such hidden dependence

    💬 0🔄 0⭐ 1
  • 💬 0🔄 0⭐ 0
  • 💬 1🔄 1⭐ 8
  • 💬 0🔄 0⭐ 4