docs: remove redundant descriptions from README.md

README.md

@@ -1,12 +1,10 @@
 # Verified Quantum Computing in Lean (vqc_in_lean)
 
-**vqc_in_lean** is a Lean 4 port of the Verified Quantum Computing (VQC) project, originally implemented using the Coq proof assistant. This project aims to provide a formal foundation for quantum computing and the verification of quantum programs using Lean 4 and mathlib4.
+**vqc_in_lean** is a Lean 4 port of the [Verified Quantum Computing (VQC) project](https://people.cs.uchicago.edu/~caldwellb/posts/2022-09-14-vqc.html), originally implemented using the Coq proof assistant. This project aims to provide a formal foundation for quantum computing and the verification of quantum programs using Lean 4 and mathlib4.
 
 ## Overview
 
-This project is inspired by the [VQC project](https://people.cs.uchicago.edu/~caldwellb/posts/2022-09-14-vqc.html), which uses Coq to teach quantum computing and program verification. **vqc_in_lean** seeks to replicate and extend this functionality in the Lean 4 ecosystem.
-
 > **Note**: This project is created as part of my personal learning journey in Lean 4 and quantum computing. It is not intended for production use or as an officially supported educational resource. Feedback and suggestions are welcome as I refine my understanding of these topics.
 
 ---
-Inspired by Ben Caldwell and Robert Rand’s [Verified Quantum Computing tutorial](https://icfp22.sigplan.org/details/icfp-2022-tutorials/2/Verified-Quantum-Computing).
+Inspired by Ben Caldwell and Robert Rand’s [Verified Quantum Computing tutorial](https://icfp22.sigplan.org/details/icfp-2022-tutorials/2/Verified-Quantum-Computing).