Questions tagged [performance]
For questions pertaining to the measurement or improvement of code and application efficiency.
5
questions
3
votes
1
answer
59
views
Are there squeeze-versions of ring and abel?
In Lean, it is recommended to use squeeze_simp to generate simp only [a bunch of lemmas] for two reasons:
(1) Otherwise the ...
- 165
10
votes
1
answer
191
views
Performance of de Bruijn indices?
Can any of you refer me to documented results of experiments on the performance of provers using de Bruijn indices to represent references to bound variables versus mentions of names or other simple ...
- 305
20
votes
0
answers
204
views
What is known about performance bottlenecks in proof assistants?
Background
In my personal experience, the biggest bottleneck to broader adoption of proof assistants (in industry and mathematics) is the effort it takes to engineer proofs. (In lines of code, for ...
- 1,327
9
votes
2
answers
252
views
Are search heuristics the main bottleneck for automated theorem provers?
My understanding of most automated theorem provers (which is possibly an incorrect understanding!) is that they start with some premises stored as unprocessed statements, and repeatedly select one to &...
- 519
13
votes
2
answers
184
views
Are there any proof assistants which integrate JITs?
Has there been notable research or attempts to integrate a JIT compiler into a proof assistant in order to achieve performance gains for proof verification, or general programming?
Whilst it may seem ...
- 566