diff --git a/content/blog/induction-lean3.md b/content/blog/induction-lean3.md
index 3e75a56..70cfc1f 100644
--- a/content/blog/induction-lean3.md
+++ b/content/blog/induction-lean3.md
@@ -1,10 +1,12 @@
 ---
-title: "Induction in Lean 3: Three Techniques"
-date: 2023-01-30T21:07:43-05:00
-draft: false 
-tags: ["Formal Methods"]
+date: 2023-01-30 21:07:43-05:00
+draft: false
 math: true
 medium_enabled: true
+medium_post_id: 5b4a36988c6d
+tags:
+- Formal Methods
+title: 'Induction in Lean 3: Three Techniques'
 ---
 
 When proving properties of an inductive data type, chances are that we need to perform the induction tactic on the data structure. There are multiple ways to approach this though and each comes with its own pros and cons.
@@ -116,4 +118,4 @@ Personally, this one is the easiest for me to follow. The main issue that I have
 
 ## Conclusion
 
-Each approach comes with its tradeoffs. The `rec_on` approach looks clean for single induction proofs. Meanwhile, the pattern matching approach works great with multiple induction. The easiest approach to determining the appropriate subgoals is to use the `induction` tactic. In fact, it sometimes is more efficient to write the entire proof via tactics first and then work towards making it more readable with additional subproofs and rewriting.
+Each approach comes with its tradeoffs. The `rec_on` approach looks clean for single induction proofs. Meanwhile, the pattern matching approach works great with multiple induction. The easiest approach to determining the appropriate subgoals is to use the `induction` tactic. In fact, it sometimes is more efficient to write the entire proof via tactics first and then work towards making it more readable with additional subproofs and rewriting.
\ No newline at end of file
diff --git a/content/blog/latex-footnote-no-count.md b/content/blog/latex-footnote-no-count.md
index c945178..b982add 100644
--- a/content/blog/latex-footnote-no-count.md
+++ b/content/blog/latex-footnote-no-count.md
@@ -1,10 +1,12 @@
 ---
-title: "Quick LaTex: Footnotes with no Counter"
-date: 2022-09-23T15:34:28-04:00
+date: 2022-09-23 15:34:28-04:00
 draft: false
-tags: ["LaTex"]
 math: false
 medium_enabled: true
+medium_post_id: d0a88900c580
+tags:
+- LaTex
+title: 'Quick LaTex: Footnotes with no Counter'
 ---
 
 Let's say there's a scenario where you want to have a footnote, but you don't want a counter associated with it. In order to stay consistent with the document style, the solution should use `\footnote` within its implementation.
@@ -52,5 +54,4 @@ Complete Minimal Example:
 
 \end{document}
 
-```
-
+```
\ No newline at end of file
diff --git a/content/blog/readable-lean3-proofs.md b/content/blog/readable-lean3-proofs.md
index 1d2b963..2be47a5 100644
--- a/content/blog/readable-lean3-proofs.md
+++ b/content/blog/readable-lean3-proofs.md
@@ -1,10 +1,12 @@
 ---
-title: "Readable Lean 3 Proofs"
-date: 2023-01-27T22:01:54-05:00
+date: 2023-01-27 22:01:54-05:00
 draft: false
-tags: ["Formal Methods"]
 math: true
 medium_enabled: true
+medium_post_id: 5fb876d4d819
+tags:
+- Formal Methods
+title: Readable Lean 3 Proofs
 ---
 
 *Important Note: This blog post uses the Lean 3 syntax*
@@ -180,4 +182,4 @@ When most people are taught how to write proofs in an interactive theorem prover
 
 We can take the guesswork out of figuring out the proof state by carefully selecting tactics which allow us to explicitely show the object being constructed. In Lean, these are `assume`, `have`, and `show`. Also making use of the inference rules themselves such as `or.elim` is a great alternative to `cases`, and `and.intro` is a great alternative to split.
 
-If you have any other techniques on making ITP proofs more readable, please let me know.
+If you have any other techniques on making ITP proofs more readable, please let me know.
\ No newline at end of file