brozek/website
1
0
Fork 0
mirror of https://github.com/Brandon-Rozek/website.git synced 2025-10-09 14:31:13 +00:00
Code Issues Projects Releases Packages Activity

Added medium syndication metadata

Browse source
This commit is contained in:
Brandon Rozek 2023-02-18 21:37:22 -05:00
parent a51e20fbc7
commit a22bb998cb
14 changed files with 78 additions and 68 deletions
Download patch file Download diff file Expand all files Collapse all files

10
content/blog/leantactics.md
View file

@ -1,10 +1,12 @@
---
title: "Lean Theorem Prover Tactics"
date: 2021-10-10T23:52:41-04:00
date: 2021-10-11 03:52:41
draft: false
tags: ["Formal Methods"]
math: false
medium_enabled: true
medium_post_id: adea1a69ddc8
tags:
- Formal Methods
title: Lean Theorem Prover Tactics
---
I've recently been playing with the Lean Theorem Prover. I am impressed with how some of the mathematics community decided to extend this project via [mathlib](https://leanprover-community.github.io/) and really make proving theorems in this framework easy and enjoyable.
@ -284,4 +286,4 @@ end
Documentation: https://leanprover-community.github.io/mathlib_docs/tactics.html#linarith
## Conclusion
A common pattern of writing proofs for me is to use a combination of `hint` and `have` with `library_search`. Especially when you are not an expert in a theorem prover, it's nice to have the system fill in some of the simpler steps. I generally prefer tactics that give you a list of simpler tactics back as opposed to solving the goal in the background without any proof. Regardless, I'm glad that many of these decision procedures exist to help me deal with what can sometimes be the verbosity of theorem proving.
A common pattern of writing proofs for me is to use a combination of `hint` and `have` with `library_search`. Especially when you are not an expert in a theorem prover, it's nice to have the system fill in some of the simpler steps. I generally prefer tactics that give you a list of simpler tactics back as opposed to solving the goal in the background without any proof. Regardless, I'm glad that many of these decision procedures exist to help me deal with what can sometimes be the verbosity of theorem proving.