Thinking about the scalability limits of dependent type…
0 reactions
Thinking about the scalability limits of dependent type systems in ITPs
I'm trying to learn as much as possible on programming language design - looking at the structural bottlenecks between interactive proof assistants (like Lean 4) and automated theorem proving. Historically, creating valid proof terms in a system based on dependent type theory is super labor-intensive. The theory itself is beautiful, but manually guiding a proof assistant through mathematical spaces scales horribly. The manual labour IS the biggest problem.
But what's cool from a theory perspective right now are the new hybrid systems that combine the absolute soundness of an ITP kernel with the search efficiency of automated provers. So instead of just relying on classic tactics these architectures are generating complex proof terms that the kernel can natively type-check. Mostly getting this from a breakdown on how automated reasoning helped formalize a disproof of an old Erdos conjecture within Lean 4 (source - https://logicalintelligence.com/blog/aleph-prover-erdos-disproof-lean-4-formal-methods )
And it does show how that if a language's type system can offload term construction to external automated search without sacrificing soundness, it changes how we approach language expressive power. And it all is way more profound than standard static analysis.
Anyone here working on the semantics of these hybrid proof environments? im looking for reading material on how they optimize the "proof reconstruction" step without blowing up the verification time.
#technology
I'm trying to learn as much as possible on programming language design - looking at the structural bottlenecks between interactive proof assistants (like Lean 4) and automated theorem proving. Historically, creating valid proof terms in a system based on dependent type theory is super labor-intensive. The theory itself is beautiful, but manually guiding a proof assistant through mathematical spaces scales horribly. The manual labour IS the biggest problem.
But what's cool from a theory perspective right now are the new hybrid systems that combine the absolute soundness of an ITP kernel with the search efficiency of automated provers. So instead of just relying on classic tactics these architectures are generating complex proof terms that the kernel can natively type-check. Mostly getting this from a breakdown on how automated reasoning helped formalize a disproof of an old Erdos conjecture within Lean 4 (source - https://logicalintelligence.com/blog/aleph-prover-erdos-disproof-lean-4-formal-methods )
And it does show how that if a language's type system can offload term construction to external automated search without sacrificing soundness, it changes how we approach language expressive power. And it all is way more profound than standard static analysis.
Anyone here working on the semantics of these hybrid proof environments? im looking for reading material on how they optimize the "proof reconstruction" step without blowing up the verification time.
#technology
| 3,000 mlx | |
| 3 | |
| 0 |