diff --git a/README.md b/README.md
index be8c88f42a96a9fc992840c17a614e4711ee7e42..146df96ceba75da0f7dcbcc314c3bb8c46e40db5 100644
--- a/README.md
+++ b/README.md
@@ -1,14 +1,19 @@
-#LISA: LISA Is Sets Automated
+# LISA = LISA Is Sets Automated
 
+LISA is a Proof Assistant based on first order logic, sequent calculus and set theory. To get started, look at the [Reference Manual](/LISA%20Reference%20Manual.pdf).
 
-## Kernel
+EPFL-LARA Website: https://lara.epfl.ch/w/
+
+## Project Organisation
+
+### Kernel
 The kernel package contains the trusted code of LISA, in the sense that it only can produce theorem and verify proof. Any bug or error in code written outside this package should not possibly break soundness.
 The kernel contains essentially two elements: Formalisation of First Order Logic, and Formalisation of Proofs through Sequent Calculus.
 
-## Proven
+### Proven
 The proven package contains tactics and proofs
 
-## TPTP
+### TPTP
 The TPTP package contains a parser from the TPTP file format to LISA. The simplest way to use it is to download the TPTP library and put it inside main/resources.
 
 ## Commands
@@ -18,8 +23,8 @@ The TPTP package contains a parser from the TPTP file format to LISA. The simple
 * `sbt doc` to generate the Scala documentation
 
 
-#LICENSE
-   Copyright [2022] [EPFL]
+## LICENSE
+   Copyright 2022 EPFL
 
    Licensed under the Apache License, Version 2.0 (the "License");
    you may not use this file except in compliance with the License.