diff --git a/.github/workflows/proof_tools.yml b/.github/workflows/proof_tools.yml
index 9621e082b514b8eb973315addc340a1da996cbef..bc19182210d7f3062801531cf0fe4ffa6747854c 100644
--- a/.github/workflows/proof_tools.yml
+++ b/.github/workflows/proof_tools.yml
@@ -54,6 +54,13 @@ jobs:
         opam exec -- dune build
         opam exec -- dune runtest
 
+    - name: autosolve
+      run: |
+        cd "${GITHUB_WORKSPACE}"/personoj/proofs/autosolve || exit 1
+        opam install cmdliner --yes
+        opam exec -- dune build
+        opam exec -- dune runtest
+
   pipeline:
     strategy:
       fail-fast: false
@@ -87,6 +94,7 @@ jobs:
         (cd qfo && bmake && sudo bmake install)
         (cd split && bmake && sudo bmake install)
         (cd pipeline && bmake && sudo bmake install)
+        (cd autosolve && bmake && sudo bmake install)
 
     - name: launch pipeline
       run: |
diff --git a/proofs/autosolve/.gitignore b/proofs/autosolve/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..6783440b6e83301a4009c0854c2492efe3491971
--- /dev/null
+++ b/proofs/autosolve/.gitignore
@@ -0,0 +1,2 @@
+psnj-autosolve
+_build
diff --git a/proofs/autosolve/.ocamlformat b/proofs/autosolve/.ocamlformat
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/proofs/autosolve/Makefile b/proofs/autosolve/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..429c35befbc9bc944826ebe17a71f4720e58defc
--- /dev/null
+++ b/proofs/autosolve/Makefile
@@ -0,0 +1,5 @@
+ROOT     = autosolve
+CMDLINER = true
+
+.include "../dune-exe.mk"
+.include "../tools.mk"
diff --git a/proofs/autosolve/autosolve.ml b/proofs/autosolve/autosolve.ml
new file mode 100644
index 0000000000000000000000000000000000000000..c63f56934b0448e469efe268d72589d10575ce32
--- /dev/null
+++ b/proofs/autosolve/autosolve.ml
@@ -0,0 +1,47 @@
+open Cmdliner
+open Common
+open Parsing
+module S = Syntax
+
+let appaxiom fixed =
+  if fixed then Format.set_geometry ~max_indent:16 ~margin:80;
+  let ast = Parser.parse stdin in
+  let process Pos.{ elt = cmd; pos } =
+    match cmd with
+    | S.P_symbol s ->
+        let script =
+          Some ([ Pos.none @@ S.P_tac_why3 None ], Pos.none @@ S.P_proof_end)
+        in
+        let cmd = S.P_symbol { s with p_sym_prf = script; p_sym_def = true } in
+        Format.printf "%a@\n" Pretty.command (Pos.make pos cmd)
+    | _ ->
+        Format.eprintf "Ill-formed input: only axioms allowed@.";
+        exit 1
+  in
+  Stream.iter process ast
+
+let fixed =
+  let doc =
+    "Fix the geometry of the output to have terminal intependant output"
+  in
+  Arg.(value & flag & info [ "fixed" ] ~doc)
+
+let cmd =
+  let doc = "Transform axioms into automatically proved theorems" in
+  let exits = Term.default_exits in
+  let man =
+    [
+      `S Manpage.s_description;
+      `P
+        "$(tname) is a filter that adds a proof script to each axioms passed \
+         on the standard input.";
+      `S Manpage.s_examples;
+      `P "Faced with input";
+      `Pre "symbol foo: TYPE;";
+      `P "$(tname) returns";
+      `Pre "symbol foo: TYPE :=\nbegin\n  why3;\nend;";
+    ]
+  in
+  (Term.(const appaxiom $ fixed), Term.info "psnj-autosolve" ~doc ~exits ~man)
+
+let () = Term.(exit @@ eval cmd)
diff --git a/proofs/autosolve/dune b/proofs/autosolve/dune
new file mode 100644
index 0000000000000000000000000000000000000000..4261f0dd6fe629c4a197535c8d6dd84e65a30660
--- /dev/null
+++ b/proofs/autosolve/dune
@@ -0,0 +1,3 @@
+(executable
+ (name autosolve)
+ (libraries cmdliner lambdapi.parsing lambdapi.common))
diff --git a/proofs/autosolve/dune-project b/proofs/autosolve/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..ae730292676bfc91a5a5e576cfbc1f333eb7df2d
--- /dev/null
+++ b/proofs/autosolve/dune-project
@@ -0,0 +1,2 @@
+(lang dune 2.9)
+(cram enable)
diff --git a/proofs/autosolve/tests/autosolve.t b/proofs/autosolve/tests/autosolve.t
new file mode 100644
index 0000000000000000000000000000000000000000..022ed716738ec4c0c94c4a3c8cefbbf7b19684dd
--- /dev/null
+++ b/proofs/autosolve/tests/autosolve.t
@@ -0,0 +1,15 @@
+  $ echo 'symbol true: foo bar baz;' | ../autosolve.exe --fixed
+  symbol true : foo bar baz ≔
+  begin
+    why3;
+  end;
+
+  $ echo 'symbol foo: TYPE; symbol bar: TYPE;' | ../autosolve.exe --fixed
+  symbol foo : TYPE ≔
+  begin
+    why3;
+  end;
+  symbol bar : TYPE ≔
+  begin
+    why3;
+  end;
diff --git a/proofs/autosolve/tests/dune b/proofs/autosolve/tests/dune
new file mode 100644
index 0000000000000000000000000000000000000000..a60e7c548b9842e4dc82503a3975c13417f75553
--- /dev/null
+++ b/proofs/autosolve/tests/dune
@@ -0,0 +1,2 @@
+(cram
+ (deps ../autosolve.exe))