diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..691da99
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,51 @@
+*.sage.py
+/fonts/
+/website/demo/
+*.png
+
+# Miscellaneous
+*.class
+*.log
+*.pyc
+*.swp
+.DS_Store
+.atom/
+.buildlog/
+.history
+.svn/
+
+# IntelliJ related
+*.iml
+*.ipr
+*.iws
+.idea/
+
+# The .vscode folder contains launch configuration and tasks you configure in
+# VS Code which you may wish to be included in version control, so this line
+# is commented out by default.
+#.vscode/
+
+# Flutter/Dart/Pub related
+**/doc/api/
+**/ios/Flutter/.last_build_id
+.dart_tool/
+.flutter-plugins
+.flutter-plugins-dependencies
+.packages
+.pub-cache/
+.pub/
+/build/
+
+# Web related
+lib/generated_plugin_registrant.dart
+
+# Symbolication related
+app.*.symbols
+
+# Obfuscation related
+app.*.map.json
+
+# Android Studio will place build artifacts here
+/android/app/debug
+/android/app/profile
+/android/app/release
diff --git a/.metadata b/.metadata
new file mode 100644
index 0000000..166a998
--- /dev/null
+++ b/.metadata
@@ -0,0 +1,10 @@
+# This file tracks properties of this Flutter project.
+# Used by Flutter tool to assess capabilities and perform upgrades etc.
+#
+# This file should be version controlled and should not be manually edited.
+
+version:
+  revision: c860cba910319332564e1e9d470a17074c1f2dfd
+  channel: stable
+
+project_type: app
diff --git a/COPYING b/COPYING
new file mode 100644
index 0000000..f288702
--- /dev/null
+++ b/COPYING
@@ -0,0 +1,674 @@
+                    GNU GENERAL PUBLIC LICENSE
+                       Version 3, 29 June 2007
+
+ Copyright (C) 2007 Free Software Foundation, Inc. <https://fsf.org/>
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+                            Preamble
+
+  The GNU General Public License is a free, copyleft license for
+software and other kinds of works.
+
+  The licenses for most software and other practical works are designed
+to take away your freedom to share and change the works.  By contrast,
+the GNU General Public License is intended to guarantee your freedom to
+share and change all versions of a program--to make sure it remains free
+software for all its users.  We, the Free Software Foundation, use the
+GNU General Public License for most of our software; it applies also to
+any other work released this way by its authors.  You can apply it to
+your programs, too.
+
+  When we speak of free software, we are referring to freedom, not
+price.  Our General Public Licenses are designed to make sure that you
+have the freedom to distribute copies of free software (and charge for
+them if you wish), that you receive source code or can get it if you
+want it, that you can change the software or use pieces of it in new
+free programs, and that you know you can do these things.
+
+  To protect your rights, we need to prevent others from denying you
+these rights or asking you to surrender the rights.  Therefore, you have
+certain responsibilities if you distribute copies of the software, or if
+you modify it: responsibilities to respect the freedom of others.
+
+  For example, if you distribute copies of such a program, whether
+gratis or for a fee, you must pass on to the recipients the same
+freedoms that you received.  You must make sure that they, too, receive
+or can get the source code.  And you must show them these terms so they
+know their rights.
+
+  Developers that use the GNU GPL protect your rights with two steps:
+(1) assert copyright on the software, and (2) offer you this License
+giving you legal permission to copy, distribute and/or modify it.
+
+  For the developers' and authors' protection, the GPL clearly explains
+that there is no warranty for this free software.  For both users' and
+authors' sake, the GPL requires that modified versions be marked as
+changed, so that their problems will not be attributed erroneously to
+authors of previous versions.
+
+  Some devices are designed to deny users access to install or run
+modified versions of the software inside them, although the manufacturer
+can do so.  This is fundamentally incompatible with the aim of
+protecting users' freedom to change the software.  The systematic
+pattern of such abuse occurs in the area of products for individuals to
+use, which is precisely where it is most unacceptable.  Therefore, we
+have designed this version of the GPL to prohibit the practice for those
+products.  If such problems arise substantially in other domains, we
+stand ready to extend this provision to those domains in future versions
+of the GPL, as needed to protect the freedom of users.
+
+  Finally, every program is threatened constantly by software patents.
+States should not allow patents to restrict development and use of
+software on general-purpose computers, but in those that do, we wish to
+avoid the special danger that patents applied to a free program could
+make it effectively proprietary.  To prevent this, the GPL assures that
+patents cannot be used to render the program non-free.
+
+  The precise terms and conditions for copying, distribution and
+modification follow.
+
+                       TERMS AND CONDITIONS
+
+  0. Definitions.
+
+  "This License" refers to version 3 of the GNU General Public License.
+
+  "Copyright" also means copyright-like laws that apply to other kinds of
+works, such as semiconductor masks.
+
+  "The Program" refers to any copyrightable work licensed under this
+License.  Each licensee is addressed as "you".  "Licensees" and
+"recipients" may be individuals or organizations.
+
+  To "modify" a work means to copy from or adapt all or part of the work
+in a fashion requiring copyright permission, other than the making of an
+exact copy.  The resulting work is called a "modified version" of the
+earlier work or a work "based on" the earlier work.
+
+  A "covered work" means either the unmodified Program or a work based
+on the Program.
+
+  To "propagate" a work means to do anything with it that, without
+permission, would make you directly or secondarily liable for
+infringement under applicable copyright law, except executing it on a
+computer or modifying a private copy.  Propagation includes copying,
+distribution (with or without modification), making available to the
+public, and in some countries other activities as well.
+
+  To "convey" a work means any kind of propagation that enables other
+parties to make or receive copies.  Mere interaction with a user through
+a computer network, with no transfer of a copy, is not conveying.
+
+  An interactive user interface displays "Appropriate Legal Notices"
+to the extent that it includes a convenient and prominently visible
+feature that (1) displays an appropriate copyright notice, and (2)
+tells the user that there is no warranty for the work (except to the
+extent that warranties are provided), that licensees may convey the
+work under this License, and how to view a copy of this License.  If
+the interface presents a list of user commands or options, such as a
+menu, a prominent item in the list meets this criterion.
+
+  1. Source Code.
+
+  The "source code" for a work means the preferred form of the work
+for making modifications to it.  "Object code" means any non-source
+form of a work.
+
+  A "Standard Interface" means an interface that either is an official
+standard defined by a recognized standards body, or, in the case of
+interfaces specified for a particular programming language, one that
+is widely used among developers working in that language.
+
+  The "System Libraries" of an executable work include anything, other
+than the work as a whole, that (a) is included in the normal form of
+packaging a Major Component, but which is not part of that Major
+Component, and (b) serves only to enable use of the work with that
+Major Component, or to implement a Standard Interface for which an
+implementation is available to the public in source code form.  A
+"Major Component", in this context, means a major essential component
+(kernel, window system, and so on) of the specific operating system
+(if any) on which the executable work runs, or a compiler used to
+produce the work, or an object code interpreter used to run it.
+
+  The "Corresponding Source" for a work in object code form means all
+the source code needed to generate, install, and (for an executable
+work) run the object code and to modify the work, including scripts to
+control those activities.  However, it does not include the work's
+System Libraries, or general-purpose tools or generally available free
+programs which are used unmodified in performing those activities but
+which are not part of the work.  For example, Corresponding Source
+includes interface definition files associated with source files for
+the work, and the source code for shared libraries and dynamically
+linked subprograms that the work is specifically designed to require,
+such as by intimate data communication or control flow between those
+subprograms and other parts of the work.
+
+  The Corresponding Source need not include anything that users
+can regenerate automatically from other parts of the Corresponding
+Source.
+
+  The Corresponding Source for a work in source code form is that
+same work.
+
+  2. Basic Permissions.
+
+  All rights granted under this License are granted for the term of
+copyright on the Program, and are irrevocable provided the stated
+conditions are met.  This License explicitly affirms your unlimited
+permission to run the unmodified Program.  The output from running a
+covered work is covered by this License only if the output, given its
+content, constitutes a covered work.  This License acknowledges your
+rights of fair use or other equivalent, as provided by copyright law.
+
+  You may make, run and propagate covered works that you do not
+convey, without conditions so long as your license otherwise remains
+in force.  You may convey covered works to others for the sole purpose
+of having them make modifications exclusively for you, or provide you
+with facilities for running those works, provided that you comply with
+the terms of this License in conveying all material for which you do
+not control copyright.  Those thus making or running the covered works
+for you must do so exclusively on your behalf, under your direction
+and control, on terms that prohibit them from making any copies of
+your copyrighted material outside their relationship with you.
+
+  Conveying under any other circumstances is permitted solely under
+the conditions stated below.  Sublicensing is not allowed; section 10
+makes it unnecessary.
+
+  3. Protecting Users' Legal Rights From Anti-Circumvention Law.
+
+  No covered work shall be deemed part of an effective technological
+measure under any applicable law fulfilling obligations under article
+11 of the WIPO copyright treaty adopted on 20 December 1996, or
+similar laws prohibiting or restricting circumvention of such
+measures.
+
+  When you convey a covered work, you waive any legal power to forbid
+circumvention of technological measures to the extent such circumvention
+is effected by exercising rights under this License with respect to
+the covered work, and you disclaim any intention to limit operation or
+modification of the work as a means of enforcing, against the work's
+users, your or third parties' legal rights to forbid circumvention of
+technological measures.
+
+  4. Conveying Verbatim Copies.
+
+  You may convey verbatim copies of the Program's source code as you
+receive it, in any medium, provided that you conspicuously and
+appropriately publish on each copy an appropriate copyright notice;
+keep intact all notices stating that this License and any
+non-permissive terms added in accord with section 7 apply to the code;
+keep intact all notices of the absence of any warranty; and give all
+recipients a copy of this License along with the Program.
+
+  You may charge any price or no price for each copy that you convey,
+and you may offer support or warranty protection for a fee.
+
+  5. Conveying Modified Source Versions.
+
+  You may convey a work based on the Program, or the modifications to
+produce it from the Program, in the form of source code under the
+terms of section 4, provided that you also meet all of these conditions:
+
+    a) The work must carry prominent notices stating that you modified
+    it, and giving a relevant date.
+
+    b) The work must carry prominent notices stating that it is
+    released under this License and any conditions added under section
+    7.  This requirement modifies the requirement in section 4 to
+    "keep intact all notices".
+
+    c) You must license the entire work, as a whole, under this
+    License to anyone who comes into possession of a copy.  This
+    License will therefore apply, along with any applicable section 7
+    additional terms, to the whole of the work, and all its parts,
+    regardless of how they are packaged.  This License gives no
+    permission to license the work in any other way, but it does not
+    invalidate such permission if you have separately received it.
+
+    d) If the work has interactive user interfaces, each must display
+    Appropriate Legal Notices; however, if the Program has interactive
+    interfaces that do not display Appropriate Legal Notices, your
+    work need not make them do so.
+
+  A compilation of a covered work with other separate and independent
+works, which are not by their nature extensions of the covered work,
+and which are not combined with it such as to form a larger program,
+in or on a volume of a storage or distribution medium, is called an
+"aggregate" if the compilation and its resulting copyright are not
+used to limit the access or legal rights of the compilation's users
+beyond what the individual works permit.  Inclusion of a covered work
+in an aggregate does not cause this License to apply to the other
+parts of the aggregate.
+
+  6. Conveying Non-Source Forms.
+
+  You may convey a covered work in object code form under the terms
+of sections 4 and 5, provided that you also convey the
+machine-readable Corresponding Source under the terms of this License,
+in one of these ways:
+
+    a) Convey the object code in, or embodied in, a physical product
+    (including a physical distribution medium), accompanied by the
+    Corresponding Source fixed on a durable physical medium
+    customarily used for software interchange.
+
+    b) Convey the object code in, or embodied in, a physical product
+    (including a physical distribution medium), accompanied by a
+    written offer, valid for at least three years and valid for as
+    long as you offer spare parts or customer support for that product
+    model, to give anyone who possesses the object code either (1) a
+    copy of the Corresponding Source for all the software in the
+    product that is covered by this License, on a durable physical
+    medium customarily used for software interchange, for a price no
+    more than your reasonable cost of physically performing this
+    conveying of source, or (2) access to copy the
+    Corresponding Source from a network server at no charge.
+
+    c) Convey individual copies of the object code with a copy of the
+    written offer to provide the Corresponding Source.  This
+    alternative is allowed only occasionally and noncommercially, and
+    only if you received the object code with such an offer, in accord
+    with subsection 6b.
+
+    d) Convey the object code by offering access from a designated
+    place (gratis or for a charge), and offer equivalent access to the
+    Corresponding Source in the same way through the same place at no
+    further charge.  You need not require recipients to copy the
+    Corresponding Source along with the object code.  If the place to
+    copy the object code is a network server, the Corresponding Source
+    may be on a different server (operated by you or a third party)
+    that supports equivalent copying facilities, provided you maintain
+    clear directions next to the object code saying where to find the
+    Corresponding Source.  Regardless of what server hosts the
+    Corresponding Source, you remain obligated to ensure that it is
+    available for as long as needed to satisfy these requirements.
+
+    e) Convey the object code using peer-to-peer transmission, provided
+    you inform other peers where the object code and Corresponding
+    Source of the work are being offered to the general public at no
+    charge under subsection 6d.
+
+  A separable portion of the object code, whose source code is excluded
+from the Corresponding Source as a System Library, need not be
+included in conveying the object code work.
+
+  A "User Product" is either (1) a "consumer product", which means any
+tangible personal property which is normally used for personal, family,
+or household purposes, or (2) anything designed or sold for incorporation
+into a dwelling.  In determining whether a product is a consumer product,
+doubtful cases shall be resolved in favor of coverage.  For a particular
+product received by a particular user, "normally used" refers to a
+typical or common use of that class of product, regardless of the status
+of the particular user or of the way in which the particular user
+actually uses, or expects or is expected to use, the product.  A product
+is a consumer product regardless of whether the product has substantial
+commercial, industrial or non-consumer uses, unless such uses represent
+the only significant mode of use of the product.
+
+  "Installation Information" for a User Product means any methods,
+procedures, authorization keys, or other information required to install
+and execute modified versions of a covered work in that User Product from
+a modified version of its Corresponding Source.  The information must
+suffice to ensure that the continued functioning of the modified object
+code is in no case prevented or interfered with solely because
+modification has been made.
+
+  If you convey an object code work under this section in, or with, or
+specifically for use in, a User Product, and the conveying occurs as
+part of a transaction in which the right of possession and use of the
+User Product is transferred to the recipient in perpetuity or for a
+fixed term (regardless of how the transaction is characterized), the
+Corresponding Source conveyed under this section must be accompanied
+by the Installation Information.  But this requirement does not apply
+if neither you nor any third party retains the ability to install
+modified object code on the User Product (for example, the work has
+been installed in ROM).
+
+  The requirement to provide Installation Information does not include a
+requirement to continue to provide support service, warranty, or updates
+for a work that has been modified or installed by the recipient, or for
+the User Product in which it has been modified or installed.  Access to a
+network may be denied when the modification itself materially and
+adversely affects the operation of the network or violates the rules and
+protocols for communication across the network.
+
+  Corresponding Source conveyed, and Installation Information provided,
+in accord with this section must be in a format that is publicly
+documented (and with an implementation available to the public in
+source code form), and must require no special password or key for
+unpacking, reading or copying.
+
+  7. Additional Terms.
+
+  "Additional permissions" are terms that supplement the terms of this
+License by making exceptions from one or more of its conditions.
+Additional permissions that are applicable to the entire Program shall
+be treated as though they were included in this License, to the extent
+that they are valid under applicable law.  If additional permissions
+apply only to part of the Program, that part may be used separately
+under those permissions, but the entire Program remains governed by
+this License without regard to the additional permissions.
+
+  When you convey a copy of a covered work, you may at your option
+remove any additional permissions from that copy, or from any part of
+it.  (Additional permissions may be written to require their own
+removal in certain cases when you modify the work.)  You may place
+additional permissions on material, added by you to a covered work,
+for which you have or can give appropriate copyright permission.
+
+  Notwithstanding any other provision of this License, for material you
+add to a covered work, you may (if authorized by the copyright holders of
+that material) supplement the terms of this License with terms:
+
+    a) Disclaiming warranty or limiting liability differently from the
+    terms of sections 15 and 16 of this License; or
+
+    b) Requiring preservation of specified reasonable legal notices or
+    author attributions in that material or in the Appropriate Legal
+    Notices displayed by works containing it; or
+
+    c) Prohibiting misrepresentation of the origin of that material, or
+    requiring that modified versions of such material be marked in
+    reasonable ways as different from the original version; or
+
+    d) Limiting the use for publicity purposes of names of licensors or
+    authors of the material; or
+
+    e) Declining to grant rights under trademark law for use of some
+    trade names, trademarks, or service marks; or
+
+    f) Requiring indemnification of licensors and authors of that
+    material by anyone who conveys the material (or modified versions of
+    it) with contractual assumptions of liability to the recipient, for
+    any liability that these contractual assumptions directly impose on
+    those licensors and authors.
+
+  All other non-permissive additional terms are considered "further
+restrictions" within the meaning of section 10.  If the Program as you
+received it, or any part of it, contains a notice stating that it is
+governed by this License along with a term that is a further
+restriction, you may remove that term.  If a license document contains
+a further restriction but permits relicensing or conveying under this
+License, you may add to a covered work material governed by the terms
+of that license document, provided that the further restriction does
+not survive such relicensing or conveying.
+
+  If you add terms to a covered work in accord with this section, you
+must place, in the relevant source files, a statement of the
+additional terms that apply to those files, or a notice indicating
+where to find the applicable terms.
+
+  Additional terms, permissive or non-permissive, may be stated in the
+form of a separately written license, or stated as exceptions;
+the above requirements apply either way.
+
+  8. Termination.
+
+  You may not propagate or modify a covered work except as expressly
+provided under this License.  Any attempt otherwise to propagate or
+modify it is void, and will automatically terminate your rights under
+this License (including any patent licenses granted under the third
+paragraph of section 11).
+
+  However, if you cease all violation of this License, then your
+license from a particular copyright holder is reinstated (a)
+provisionally, unless and until the copyright holder explicitly and
+finally terminates your license, and (b) permanently, if the copyright
+holder fails to notify you of the violation by some reasonable means
+prior to 60 days after the cessation.
+
+  Moreover, your license from a particular copyright holder is
+reinstated permanently if the copyright holder notifies you of the
+violation by some reasonable means, this is the first time you have
+received notice of violation of this License (for any work) from that
+copyright holder, and you cure the violation prior to 30 days after
+your receipt of the notice.
+
+  Termination of your rights under this section does not terminate the
+licenses of parties who have received copies or rights from you under
+this License.  If your rights have been terminated and not permanently
+reinstated, you do not qualify to receive new licenses for the same
+material under section 10.
+
+  9. Acceptance Not Required for Having Copies.
+
+  You are not required to accept this License in order to receive or
+run a copy of the Program.  Ancillary propagation of a covered work
+occurring solely as a consequence of using peer-to-peer transmission
+to receive a copy likewise does not require acceptance.  However,
+nothing other than this License grants you permission to propagate or
+modify any covered work.  These actions infringe copyright if you do
+not accept this License.  Therefore, by modifying or propagating a
+covered work, you indicate your acceptance of this License to do so.
+
+  10. Automatic Licensing of Downstream Recipients.
+
+  Each time you convey a covered work, the recipient automatically
+receives a license from the original licensors, to run, modify and
+propagate that work, subject to this License.  You are not responsible
+for enforcing compliance by third parties with this License.
+
+  An "entity transaction" is a transaction transferring control of an
+organization, or substantially all assets of one, or subdividing an
+organization, or merging organizations.  If propagation of a covered
+work results from an entity transaction, each party to that
+transaction who receives a copy of the work also receives whatever
+licenses to the work the party's predecessor in interest had or could
+give under the previous paragraph, plus a right to possession of the
+Corresponding Source of the work from the predecessor in interest, if
+the predecessor has it or can get it with reasonable efforts.
+
+  You may not impose any further restrictions on the exercise of the
+rights granted or affirmed under this License.  For example, you may
+not impose a license fee, royalty, or other charge for exercise of
+rights granted under this License, and you may not initiate litigation
+(including a cross-claim or counterclaim in a lawsuit) alleging that
+any patent claim is infringed by making, using, selling, offering for
+sale, or importing the Program or any portion of it.
+
+  11. Patents.
+
+  A "contributor" is a copyright holder who authorizes use under this
+License of the Program or a work on which the Program is based.  The
+work thus licensed is called the contributor's "contributor version".
+
+  A contributor's "essential patent claims" are all patent claims
+owned or controlled by the contributor, whether already acquired or
+hereafter acquired, that would be infringed by some manner, permitted
+by this License, of making, using, or selling its contributor version,
+but do not include claims that would be infringed only as a
+consequence of further modification of the contributor version.  For
+purposes of this definition, "control" includes the right to grant
+patent sublicenses in a manner consistent with the requirements of
+this License.
+
+  Each contributor grants you a non-exclusive, worldwide, royalty-free
+patent license under the contributor's essential patent claims, to
+make, use, sell, offer for sale, import and otherwise run, modify and
+propagate the contents of its contributor version.
+
+  In the following three paragraphs, a "patent license" is any express
+agreement or commitment, however denominated, not to enforce a patent
+(such as an express permission to practice a patent or covenant not to
+sue for patent infringement).  To "grant" such a patent license to a
+party means to make such an agreement or commitment not to enforce a
+patent against the party.
+
+  If you convey a covered work, knowingly relying on a patent license,
+and the Corresponding Source of the work is not available for anyone
+to copy, free of charge and under the terms of this License, through a
+publicly available network server or other readily accessible means,
+then you must either (1) cause the Corresponding Source to be so
+available, or (2) arrange to deprive yourself of the benefit of the
+patent license for this particular work, or (3) arrange, in a manner
+consistent with the requirements of this License, to extend the patent
+license to downstream recipients.  "Knowingly relying" means you have
+actual knowledge that, but for the patent license, your conveying the
+covered work in a country, or your recipient's use of the covered work
+in a country, would infringe one or more identifiable patents in that
+country that you have reason to believe are valid.
+
+  If, pursuant to or in connection with a single transaction or
+arrangement, you convey, or propagate by procuring conveyance of, a
+covered work, and grant a patent license to some of the parties
+receiving the covered work authorizing them to use, propagate, modify
+or convey a specific copy of the covered work, then the patent license
+you grant is automatically extended to all recipients of the covered
+work and works based on it.
+
+  A patent license is "discriminatory" if it does not include within
+the scope of its coverage, prohibits the exercise of, or is
+conditioned on the non-exercise of one or more of the rights that are
+specifically granted under this License.  You may not convey a covered
+work if you are a party to an arrangement with a third party that is
+in the business of distributing software, under which you make payment
+to the third party based on the extent of your activity of conveying
+the work, and under which the third party grants, to any of the
+parties who would receive the covered work from you, a discriminatory
+patent license (a) in connection with copies of the covered work
+conveyed by you (or copies made from those copies), or (b) primarily
+for and in connection with specific products or compilations that
+contain the covered work, unless you entered into that arrangement,
+or that patent license was granted, prior to 28 March 2007.
+
+  Nothing in this License shall be construed as excluding or limiting
+any implied license or other defenses to infringement that may
+otherwise be available to you under applicable patent law.
+
+  12. No Surrender of Others' Freedom.
+
+  If conditions are imposed on you (whether by court order, agreement or
+otherwise) that contradict the conditions of this License, they do not
+excuse you from the conditions of this License.  If you cannot convey a
+covered work so as to satisfy simultaneously your obligations under this
+License and any other pertinent obligations, then as a consequence you may
+not convey it at all.  For example, if you agree to terms that obligate you
+to collect a royalty for further conveying from those to whom you convey
+the Program, the only way you could satisfy both those terms and this
+License would be to refrain entirely from conveying the Program.
+
+  13. Use with the GNU Affero General Public License.
+
+  Notwithstanding any other provision of this License, you have
+permission to link or combine any covered work with a work licensed
+under version 3 of the GNU Affero General Public License into a single
+combined work, and to convey the resulting work.  The terms of this
+License will continue to apply to the part which is the covered work,
+but the special requirements of the GNU Affero General Public License,
+section 13, concerning interaction through a network will apply to the
+combination as such.
+
+  14. Revised Versions of this License.
+
+  The Free Software Foundation may publish revised and/or new versions of
+the GNU General Public License from time to time.  Such new versions will
+be similar in spirit to the present version, but may differ in detail to
+address new problems or concerns.
+
+  Each version is given a distinguishing version number.  If the
+Program specifies that a certain numbered version of the GNU General
+Public License "or any later version" applies to it, you have the
+option of following the terms and conditions either of that numbered
+version or of any later version published by the Free Software
+Foundation.  If the Program does not specify a version number of the
+GNU General Public License, you may choose any version ever published
+by the Free Software Foundation.
+
+  If the Program specifies that a proxy can decide which future
+versions of the GNU General Public License can be used, that proxy's
+public statement of acceptance of a version permanently authorizes you
+to choose that version for the Program.
+
+  Later license versions may give you additional or different
+permissions.  However, no additional obligations are imposed on any
+author or copyright holder as a result of your choosing to follow a
+later version.
+
+  15. Disclaimer of Warranty.
+
+  THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY
+APPLICABLE LAW.  EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT
+HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY
+OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO,
+THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
+PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM
+IS WITH YOU.  SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF
+ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
+
+  16. Limitation of Liability.
+
+  IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING
+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS
+THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY
+GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE
+USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF
+DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD
+PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS),
+EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF
+SUCH DAMAGES.
+
+  17. Interpretation of Sections 15 and 16.
+
+  If the disclaimer of warranty and limitation of liability provided
+above cannot be given local legal effect according to their terms,
+reviewing courts shall apply local law that most closely approximates
+an absolute waiver of all civil liability in connection with the
+Program, unless a warranty or assumption of liability accompanies a
+copy of the Program in return for a fee.
+
+                     END OF TERMS AND CONDITIONS
+
+            How to Apply These Terms to Your New Programs
+
+  If you develop a new program, and you want it to be of the greatest
+possible use to the public, the best way to achieve this is to make it
+free software which everyone can redistribute and change under these terms.
+
+  To do so, attach the following notices to the program.  It is safest
+to attach them to the start of each source file to most effectively
+state the exclusion of warranty; and each file should have at least
+the "copyright" line and a pointer to where the full notice is found.
+
+    <one line to give the program's name and a brief idea of what it does.>
+    Copyright (C) <year>  <name of author>
+
+    This program is free software: you can redistribute it and/or modify
+    it under the terms of the GNU General Public License as published by
+    the Free Software Foundation, either version 3 of the License, or
+    (at your option) any later version.
+
+    This program is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+    GNU General Public License for more details.
+
+    You should have received a copy of the GNU General Public License
+    along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
+Also add information on how to contact you by electronic and paper mail.
+
+  If the program does terminal interaction, make it output a short
+notice like this when it starts in an interactive mode:
+
+    <program>  Copyright (C) <year>  <name of author>
+    This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'.
+    This is free software, and you are welcome to redistribute it
+    under certain conditions; type `show c' for details.
+
+The hypothetical commands `show w' and `show c' should show the appropriate
+parts of the General Public License.  Of course, your program's commands
+might be different; for a GUI interface, you would use an "about box".
+
+  You should also get your employer (if you work as a programmer) or school,
+if any, to sign a "copyright disclaimer" for the program, if necessary.
+For more information on this, and how to apply and follow the GNU GPL, see
+<https://www.gnu.org/licenses/>.
+
+  The GNU General Public License does not permit incorporating your program
+into proprietary programs.  If your program is a subroutine library, you
+may consider it more useful to permit linking proprietary applications with
+the library.  If this is what you want to do, use the GNU Lesser General
+Public License instead of this License.  But first, please read
+<https://www.gnu.org/licenses/why-not-lgpl.html>.
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..adb670b
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,42 @@
+all: app web
+app: fonts icons
+	flutter build apk
+web:
+	flutter build web --base-href='/demo/' --release
+	rm -rf website/demo/
+	cp -p -r build/web/ website/demo/
+host:
+	cd website && python -m http.server 8000
+run: fonts icons
+	flutter run
+test:
+	flutter test test/expressions_test.dart
+zip:
+	rm -f everest.zip
+	zip -r everest.zip . -x '/.git/*' -x '/.dart_tool/*' -x '/.idea/*' -x '/build/*'
+
+icons: android/app/src/main/res/mipmap-hdpi/ic_launcher.png website/favicon.ico web/favicon.ico web/icons/Icon-192.png web/icons/Icon-maskable-192.png web/icons/Icon-512.png web/icons/Icon-maskable-512.png
+android/app/src/main/res/mipmap-hdpi/ic_launcher.png: assets/launcher_icon.png
+	flutter pub get
+	flutter pub run flutter_launcher_icons:main
+assets/launcher_icon.png: assets/launcher_icon.svg
+	inkscape -w 1024 -h 1024 assets/launcher_icon.svg -o assets/launcher_icon.png
+web/favicon.ico website/favicon.ico: assets/launcher_icon.svg
+	magick -background none assets/launcher_icon.svg -define icon:auto-resize $@
+web/icons/Icon-192.png web/icons/Icon-maskable-192.png: assets/launcher_icon.svg
+	mkdir -p web/icons/
+	inkscape -w 192 -h 192 assets/launcher_icon.svg -o $@
+web/icons/Icon-512.png web/icons/Icon-maskable-512.png: assets/launcher_icon.svg
+	mkdir -p web/icons/
+	inkscape -w 512 -h 512 assets/launcher_icon.svg -o $@
+
+fonts: fonts/NotoSansMath-Regular.ttf
+fonts/NotoSansMath-Regular.ttf: | build/upstream/Noto_Sans_Math.zip
+	mkdir -p fonts/
+	unzip -o build/upstream/Noto_Sans_Math.zip -d fonts/
+build/upstream/Noto_Sans_Math.zip:
+	mkdir -p build/upstream/
+	wget -O build/upstream/Noto_Sans_Math.zip https://fonts.google.com/download?family=Noto%20Sans%20Math
+.INTERMEDIATE: build/upstream/Noto_Sans_Math.zip
+
+.PHONY: all app web host run test zip fonts icons
diff --git a/android/.gitignore b/android/.gitignore
new file mode 100644
index 0000000..6f56801
--- /dev/null
+++ b/android/.gitignore
@@ -0,0 +1,13 @@
+gradle-wrapper.jar
+/.gradle
+/captures/
+/gradlew
+/gradlew.bat
+/local.properties
+GeneratedPluginRegistrant.java
+
+# Remember to never publicly share your keystore.
+# See https://flutter.dev/docs/deployment/android#reference-the-keystore-from-the-app
+key.properties
+**/*.keystore
+**/*.jks
diff --git a/android/README.md b/android/README.md
new file mode 100644
index 0000000..b39db57
--- /dev/null
+++ b/android/README.md
@@ -0,0 +1 @@
+The files in this directory were mostly generated by Flutter.
diff --git a/android/app/build.gradle b/android/app/build.gradle
new file mode 100644
index 0000000..51aa8d8
--- /dev/null
+++ b/android/app/build.gradle
@@ -0,0 +1,69 @@
+def localProperties = new Properties()
+def localPropertiesFile = rootProject.file('local.properties')
+if (localPropertiesFile.exists()) {
+    localPropertiesFile.withReader('UTF-8') { reader ->
+        localProperties.load(reader)
+    }
+}
+
+def flutterRoot = localProperties.getProperty('flutter.sdk')
+if (flutterRoot == null) {
+    throw new GradleException("Flutter SDK not found. Define location with flutter.sdk in the local.properties file.")
+}
+
+def flutterVersionCode = localProperties.getProperty('flutter.versionCode')
+if (flutterVersionCode == null) {
+    flutterVersionCode = '1'
+}
+
+def flutterVersionName = localProperties.getProperty('flutter.versionName')
+if (flutterVersionName == null) {
+    flutterVersionName = '1.0'
+}
+
+apply plugin: 'com.android.application'
+apply plugin: 'kotlin-android'
+apply from: "$flutterRoot/packages/flutter_tools/gradle/flutter.gradle"
+
+android {
+    compileSdkVersion flutter.compileSdkVersion
+
+    compileOptions {
+        sourceCompatibility JavaVersion.VERSION_1_8
+        targetCompatibility JavaVersion.VERSION_1_8
+    }
+
+    kotlinOptions {
+        jvmTarget = '1.8'
+    }
+
+    sourceSets {
+        main.java.srcDirs += 'src/main/kotlin'
+    }
+
+    defaultConfig {
+        applicationId "io.github.mwageringel.everest"
+        // TODO workaround for https://github.com/fluttercommunity/flutter_launcher_icons/issues/324
+        minSdkVersion 16
+        // minSdkVersion flutter.minSdkVersion
+        targetSdkVersion flutter.targetSdkVersion
+        versionCode flutterVersionCode.toInteger()
+        versionName flutterVersionName
+    }
+
+    buildTypes {
+        release {
+            // TODO: Add your own signing config for the release build.
+            // Signing with the debug keys for now, so `flutter run --release` works.
+            signingConfig signingConfigs.debug
+        }
+    }
+}
+
+flutter {
+    source '../..'
+}
+
+dependencies {
+    implementation "org.jetbrains.kotlin:kotlin-stdlib-jdk7:$kotlin_version"
+}
diff --git a/android/app/src/debug/AndroidManifest.xml b/android/app/src/debug/AndroidManifest.xml
new file mode 100644
index 0000000..efd3e5c
--- /dev/null
+++ b/android/app/src/debug/AndroidManifest.xml
@@ -0,0 +1,7 @@
+<manifest xmlns:android="http://schemas.android.com/apk/res/android"
+    package="io.github.mwageringel.everest">
+    <!-- Flutter needs it to communicate with the running application
+         to allow setting breakpoints, to provide hot reload, etc.
+    -->
+    <uses-permission android:name="android.permission.INTERNET"/>
+</manifest>
diff --git a/android/app/src/main/AndroidManifest.xml b/android/app/src/main/AndroidManifest.xml
new file mode 100644
index 0000000..622561d
--- /dev/null
+++ b/android/app/src/main/AndroidManifest.xml
@@ -0,0 +1,34 @@
+<manifest xmlns:android="http://schemas.android.com/apk/res/android"
+    package="io.github.mwageringel.everest">
+   <application
+        android:label="Everest"
+        android:name="${applicationName}"
+        android:icon="@mipmap/ic_launcher">
+        <activity
+            android:name=".MainActivity"
+            android:exported="true"
+            android:launchMode="singleTop"
+            android:theme="@style/LaunchTheme"
+            android:configChanges="orientation|keyboardHidden|keyboard|screenSize|smallestScreenSize|locale|layoutDirection|fontScale|screenLayout|density|uiMode"
+            android:hardwareAccelerated="true"
+            android:windowSoftInputMode="adjustResize">
+            <!-- Specifies an Android theme to apply to this Activity as soon as
+                 the Android process has started. This theme is visible to the user
+                 while the Flutter UI initializes. After that, this theme continues
+                 to determine the Window background behind the Flutter UI. -->
+            <meta-data
+              android:name="io.flutter.embedding.android.NormalTheme"
+              android:resource="@style/NormalTheme"
+              />
+            <intent-filter>
+                <action android:name="android.intent.action.MAIN"/>
+                <category android:name="android.intent.category.LAUNCHER"/>
+            </intent-filter>
+        </activity>
+        <!-- Don't delete the meta-data below.
+             This is used by the Flutter tool to generate GeneratedPluginRegistrant.java -->
+        <meta-data
+            android:name="flutterEmbedding"
+            android:value="2" />
+    </application>
+</manifest>
diff --git a/android/app/src/main/kotlin/io/github/mwageringel/everest/MainActivity.kt b/android/app/src/main/kotlin/io/github/mwageringel/everest/MainActivity.kt
new file mode 100644
index 0000000..e6ab2e6
--- /dev/null
+++ b/android/app/src/main/kotlin/io/github/mwageringel/everest/MainActivity.kt
@@ -0,0 +1,6 @@
+package io.github.mwageringel.everest
+
+import io.flutter.embedding.android.FlutterActivity
+
+class MainActivity: FlutterActivity() {
+}
diff --git a/android/app/src/main/res/drawable-v21/launch_background.xml b/android/app/src/main/res/drawable-v21/launch_background.xml
new file mode 100644
index 0000000..f74085f
--- /dev/null
+++ b/android/app/src/main/res/drawable-v21/launch_background.xml
@@ -0,0 +1,12 @@
+<?xml version="1.0" encoding="utf-8"?>
+<!-- Modify this file to customize your launch splash screen -->
+<layer-list xmlns:android="http://schemas.android.com/apk/res/android">
+    <item android:drawable="?android:colorBackground" />
+
+    <!-- You can insert your own image assets here -->
+    <!-- <item>
+        <bitmap
+            android:gravity="center"
+            android:src="@mipmap/launch_image" />
+    </item> -->
+</layer-list>
diff --git a/android/app/src/main/res/drawable/launch_background.xml b/android/app/src/main/res/drawable/launch_background.xml
new file mode 100644
index 0000000..304732f
--- /dev/null
+++ b/android/app/src/main/res/drawable/launch_background.xml
@@ -0,0 +1,12 @@
+<?xml version="1.0" encoding="utf-8"?>
+<!-- Modify this file to customize your launch splash screen -->
+<layer-list xmlns:android="http://schemas.android.com/apk/res/android">
+    <item android:drawable="@android:color/white" />
+
+    <!-- You can insert your own image assets here -->
+    <!-- <item>
+        <bitmap
+            android:gravity="center"
+            android:src="@mipmap/launch_image" />
+    </item> -->
+</layer-list>
diff --git a/android/app/src/main/res/values-night/styles.xml b/android/app/src/main/res/values-night/styles.xml
new file mode 100644
index 0000000..3db14bb
--- /dev/null
+++ b/android/app/src/main/res/values-night/styles.xml
@@ -0,0 +1,18 @@
+<?xml version="1.0" encoding="utf-8"?>
+<resources>
+    <!-- Theme applied to the Android Window while the process is starting when the OS's Dark Mode setting is on -->
+    <style name="LaunchTheme" parent="@android:style/Theme.Black.NoTitleBar">
+        <!-- Show a splash screen on the activity. Automatically removed when
+             Flutter draws its first frame -->
+        <item name="android:windowBackground">@drawable/launch_background</item>
+    </style>
+    <!-- Theme applied to the Android Window as soon as the process has started.
+         This theme determines the color of the Android Window while your
+         Flutter UI initializes, as well as behind your Flutter UI while its
+         running.
+
+         This Theme is only used starting with V2 of Flutter's Android embedding. -->
+    <style name="NormalTheme" parent="@android:style/Theme.Black.NoTitleBar">
+        <item name="android:windowBackground">?android:colorBackground</item>
+    </style>
+</resources>
diff --git a/android/app/src/main/res/values/styles.xml b/android/app/src/main/res/values/styles.xml
new file mode 100644
index 0000000..d460d1e
--- /dev/null
+++ b/android/app/src/main/res/values/styles.xml
@@ -0,0 +1,18 @@
+<?xml version="1.0" encoding="utf-8"?>
+<resources>
+    <!-- Theme applied to the Android Window while the process is starting when the OS's Dark Mode setting is off -->
+    <style name="LaunchTheme" parent="@android:style/Theme.Light.NoTitleBar">
+        <!-- Show a splash screen on the activity. Automatically removed when
+             Flutter draws its first frame -->
+        <item name="android:windowBackground">@drawable/launch_background</item>
+    </style>
+    <!-- Theme applied to the Android Window as soon as the process has started.
+         This theme determines the color of the Android Window while your
+         Flutter UI initializes, as well as behind your Flutter UI while its
+         running.
+
+         This Theme is only used starting with V2 of Flutter's Android embedding. -->
+    <style name="NormalTheme" parent="@android:style/Theme.Light.NoTitleBar">
+        <item name="android:windowBackground">?android:colorBackground</item>
+    </style>
+</resources>
diff --git a/android/app/src/profile/AndroidManifest.xml b/android/app/src/profile/AndroidManifest.xml
new file mode 100644
index 0000000..efd3e5c
--- /dev/null
+++ b/android/app/src/profile/AndroidManifest.xml
@@ -0,0 +1,7 @@
+<manifest xmlns:android="http://schemas.android.com/apk/res/android"
+    package="io.github.mwageringel.everest">
+    <!-- Flutter needs it to communicate with the running application
+         to allow setting breakpoints, to provide hot reload, etc.
+    -->
+    <uses-permission android:name="android.permission.INTERNET"/>
+</manifest>
diff --git a/android/build.gradle b/android/build.gradle
new file mode 100644
index 0000000..4256f91
--- /dev/null
+++ b/android/build.gradle
@@ -0,0 +1,31 @@
+buildscript {
+    ext.kotlin_version = '1.6.10'
+    repositories {
+        google()
+        mavenCentral()
+    }
+
+    dependencies {
+        classpath 'com.android.tools.build:gradle:4.1.0'
+        classpath "org.jetbrains.kotlin:kotlin-gradle-plugin:$kotlin_version"
+    }
+}
+
+allprojects {
+    repositories {
+        google()
+        mavenCentral()
+    }
+}
+
+rootProject.buildDir = '../build'
+subprojects {
+    project.buildDir = "${rootProject.buildDir}/${project.name}"
+}
+subprojects {
+    project.evaluationDependsOn(':app')
+}
+
+task clean(type: Delete) {
+    delete rootProject.buildDir
+}
diff --git a/android/gradle.properties b/android/gradle.properties
new file mode 100644
index 0000000..94adc3a
--- /dev/null
+++ b/android/gradle.properties
@@ -0,0 +1,3 @@
+org.gradle.jvmargs=-Xmx1536M
+android.useAndroidX=true
+android.enableJetifier=true
diff --git a/android/gradle/wrapper/gradle-wrapper.properties b/android/gradle/wrapper/gradle-wrapper.properties
new file mode 100644
index 0000000..bc6a58a
--- /dev/null
+++ b/android/gradle/wrapper/gradle-wrapper.properties
@@ -0,0 +1,6 @@
+#Fri Jun 23 08:50:38 CEST 2017
+distributionBase=GRADLE_USER_HOME
+distributionPath=wrapper/dists
+zipStoreBase=GRADLE_USER_HOME
+zipStorePath=wrapper/dists
+distributionUrl=https\://services.gradle.org/distributions/gradle-6.7-all.zip
diff --git a/android/settings.gradle b/android/settings.gradle
new file mode 100644
index 0000000..44e62bc
--- /dev/null
+++ b/android/settings.gradle
@@ -0,0 +1,11 @@
+include ':app'
+
+def localPropertiesFile = new File(rootProject.projectDir, "local.properties")
+def properties = new Properties()
+
+assert localPropertiesFile.exists()
+localPropertiesFile.withReader("UTF-8") { reader -> properties.load(reader) }
+
+def flutterSdkPath = properties.getProperty("flutter.sdk")
+assert flutterSdkPath != null, "flutter.sdk not set in local.properties"
+apply from: "$flutterSdkPath/packages/flutter_tools/gradle/app_plugin_loader.gradle"
diff --git a/assets/launcher_icon.svg b/assets/launcher_icon.svg
new file mode 100644
index 0000000..7397272
--- /dev/null
+++ b/assets/launcher_icon.svg
@@ -0,0 +1,71 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!-- Created with Inkscape (http://www.inkscape.org/) -->
+
+<svg
+   width="1024"
+   height="1024"
+   viewBox="0 0 60.235294 60.235294"
+   version="1.1"
+   id="svg1791"
+   inkscape:version="1.2 (dc2aedaf03, 2022-05-15)"
+   sodipodi:docname="launcher_icon.svg"
+   xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+   xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+   xmlns="http://www.w3.org/2000/svg"
+   xmlns:svg="http://www.w3.org/2000/svg">
+  <sodipodi:namedview
+     id="namedview1793"
+     pagecolor="#ffffff"
+     bordercolor="#000000"
+     borderopacity="0.25"
+     inkscape:showpageshadow="2"
+     inkscape:pageopacity="0.0"
+     inkscape:pagecheckerboard="true"
+     inkscape:deskcolor="#d1d1d1"
+     inkscape:document-units="mm"
+     showgrid="false"
+     inkscape:zoom="0.70710678"
+     inkscape:cx="523.96612"
+     inkscape:cy="548.00776"
+     inkscape:window-width="1918"
+     inkscape:window-height="1078"
+     inkscape:window-x="1280"
+     inkscape:window-y="0"
+     inkscape:window-maximized="1"
+     inkscape:current-layer="layer1" />
+  <defs
+     id="defs1788">
+    <rect
+       x="170.52023"
+       y="338.1077"
+       width="88.363831"
+       height="161.03641"
+       id="rect1481" />
+  </defs>
+  <g
+     inkscape:label="Layer 1"
+     inkscape:groupmode="layer"
+     id="layer1"
+     transform="translate(-504.87587,-532.57763)">
+    <path
+       style="fill:#3f51b5;fill-opacity:1;stroke-width:0.285539"
+       d="m 509.01706,581.42615 20.13468,-38.489 8.68432,14.67487 4.08111,-7.04632 18.78881,30.82224 z"
+       id="path63"
+       sodipodi:nodetypes="cccccc" />
+    <text
+       xml:space="preserve"
+       transform="matrix(0.31140734,0,0,0.32847661,468.13014,431.92563)"
+       id="text1479"
+       style="font-size:128px;white-space:pre;shape-inside:url(#rect1481);shape-padding:0.241668;display:inline;fill:#f2f2f2;fill-opacity:1"><tspan
+         x="170.76172"
+         y="454.72856"
+         id="tspan965"><tspan
+           style="font-family:'Libertinus Math';-inkscape-font-specification:'Libertinus Math'"
+           id="tspan963">≡</tspan></tspan></text>
+    <path
+       style="fill:#000000;fill-opacity:0.12;stroke-width:0.0634825"
+       d="m 537.8353,557.6165 -12.8523,23.79778 26.95684,-0.02 z"
+       id="path2039"
+       sodipodi:nodetypes="cccc" />
+  </g>
+</svg>
diff --git a/lib/expressions.dart b/lib/expressions.dart
new file mode 100644
index 0000000..b1c3ae2
--- /dev/null
+++ b/lib/expressions.dart
@@ -0,0 +1,139 @@
+// expression algebra with variables, constants and unary and binary operations.
+
+A _evalMult<A>(A left, A right) => (left as dynamic) * right;
+
+typedef EvalContext = Map<Var<dynamic>, dynamic>;  // all our variables will have type parameter F
+
+abstract class Expression<A> {
+  String str(EvalContext vars);
+  A eval(EvalContext vars);
+  String evalString(EvalContext vars) => '[${str(vars)}] = ${eval(vars)}';  // for debugging
+  @override toString() => str({});
+
+  Expression<bool>      eq(Expression<A> other) => Bin(this, other, str: (s, t) => '$s = $t', eval: (a, b) => (a as dynamic).pow(1331) == (b as dynamic).pow(p));
+  Expression<A> operator +(Expression<A> other) => Bin(this, other, str: (s, t) => '$s + $t', eval: (a, b) => (a as dynamic) + b);
+  Expression<A> operator -(Expression<A> other) => Bin(this, other, str: (s, t) => '$s - $t', eval: (a, b) => (a as dynamic) - b);
+  Expression<A> operator *(Expression<A> other) => Bin(this, other, str: (s, t) => '$s * $t', eval: _evalMult);
+  Expression<A> operator /(Expression<A> other) => Bin(this, other, str: (s, t) => '$s / $t', eval: (a, b) => (a as dynamic) / b);
+  Expression<A> operator -() => Unary(this, str: (s) => '-$s', eval: (a) => -(a as dynamic));
+  Expression<A> square() => Unary(this, str: (s) => '$s²', eval: (A a) => _evalMult(a, a));
+  // Expression<A> paren() => Unary(this, str: (s) => '($s)', eval: (A a) => a);  // not needed yet
+}
+
+class Var<A> extends Expression<A> {
+  @override str(vars) => vars[this]?.toString() ?? '?';
+  @override eval(vars) {
+    final a = vars[this];
+    if (a == null) {
+      throw UnsupportedError('can only evaluate variables in vars context');
+    } else {
+      return a;
+    }
+  }
+}
+
+class Con<A> extends Expression<A> {
+  final A con;
+  final String? _str;
+  Con(this.con, {String? str}) : _str = str;
+  @override str(vars) => _str ?? con.toString();
+  @override eval(vars) => con;
+}
+
+class Bin<A, B> extends Expression<B> {
+  final Expression<A> left, right;
+  final B Function(A, A) _eval;
+  final String Function(String, String) _str;
+  Bin(this.left, this.right, {required B Function(A, A) eval, required String Function(String, String) str}):
+    _eval = eval, _str = str;
+  @override str(vars) => _str(left.str(vars), right.str(vars));
+  @override eval(vars) => _eval(left.eval(vars), right.eval(vars));
+}
+
+class Unary<A, B> extends Expression<B> {
+  final Expression<A> operand;
+  final B Function(A) _eval;
+  final String Function(String) _str;
+  Unary(this.operand, {required B Function(A) eval, required String Function(String) str}):
+    _eval = eval, _str = str;
+  @override str(vars) => _str(operand.str(vars));
+  @override eval(vars) => _eval(operand.eval(vars));
+}
+
+A _pow<A>(A x, int n) {
+  if (n <= 0) {
+    throw UnsupportedError("exponent must be positive");
+  } else {
+    A? res;  // iterated squaring without 1
+    while (n > 0) {
+      if (n.isOdd) {
+        res = res == null ? x : _evalMult(res, x);
+      }
+      x = _evalMult(x , x);
+      n = n ~/ 2;
+    }
+    return res as A;  // res is never null
+  }
+}
+
+const int p = 11;
+class F {
+  final int _u;
+  F._mkF(this._u);
+  static final List<F> elems = List.unmodifiable(List.generate(p, F._mkF));
+  factory F(int u) => elems[u % p];
+  factory F.parse(String s) => s == 'X' ? X.con : F(int.parse(s));
+  @override toString() => _u.toString();
+  @override operator ==(other) => other is F ? _u == other._u : false;
+  @override int get hashCode => _u.hashCode;
+  F operator +(F other) => F(_u + other._u);
+  F operator *(F other) => F(_u * other._u);
+  F operator -(F other) => F(_u - other._u);
+  F operator -() => F(-_u);
+  F pow(int exponent) => F(_u.modPow(exponent, p));
+  F operator /(F other) => this * other.pow(p-2);  // ignoring 0
+}
+
+class G {
+  final F a, b;
+  G(this.a, this.b);
+  factory G.F(int a, int b) => G(F(a), F(b));
+  factory G.fromF(F a) => G(a, F(0));
+  @override toString() => '($a,$b)';
+  @override operator ==(other) => other is G ? a == other.a && b == other.b : false;
+  @override int get hashCode => b.hashCode * p + a.hashCode;
+  G operator +(G other) => G(a + other.a, b + other.b);
+  G operator *(G other) {
+    final c = other.a, d = other.b;
+    return G(a*c + F(9)*b*d, b*c + (F(4)*b + a)*d);
+  }
+  G operator -() => G(-a, -b);
+  G operator -(G other) => this + -other;
+  G pow(int exponent) => _pow(this, exponent);
+  G operator /(G other) => this * other.pow(119);  // ignoring 0 (so `other` must not be user input)
+}
+
+final X = Con(F(7).pow(35), str: 'X');
+
+Expression<F> C(int u) => Con(F(u));
+
+Expression<F> _toExprF(x) {
+  if (x is Expression) {
+    return x as Expression<F>;
+  } else if (x is F) {
+    return Con(x);
+  } else if (x is int) {
+    return Con(F(x));
+  } else {
+    throw UnsupportedError("$x not viewable as Expression<F>");
+  }
+}
+
+final G _s = G.F(3, 3);
+
+Expression<G> dot(left, right) {
+  return Bin<F, G>(_toExprF(left), _toExprF(right),
+    eval: (a, b) => G(b + F(6)*a, a + b) * _s,
+    str: (s, t) => '$s.$t',
+  );
+}
diff --git a/lib/game.dart b/lib/game.dart
new file mode 100644
index 0000000..07b972d
--- /dev/null
+++ b/lib/game.dart
@@ -0,0 +1,556 @@
+import 'dart:async';
+import 'package:flutter/foundation.dart' show listEquals, ChangeNotifier;
+import 'package:sqflite/sqflite.dart';
+import 'package:everest/expressions.dart';
+
+const debugUnlockAll = false;
+const String tableKV = 'keyvalues', tableAnswers = 'answers';
+const String columnKey = 'key', columnValue = 'value', columnId = 'id', columnLevel = 'level', columnQuestion = 'question', columnInputs = 'inputs';
+const String levelsUnlockedKey = 'game:levelsUnlocked';
+
+enum QuestionsStatus { wrong, partial, correct }
+QuestionsStatus combineStatus(QuestionsStatus a, QuestionsStatus b) {
+  if (a == QuestionsStatus.correct) {
+    return b;
+  } else if (a == QuestionsStatus.partial || b == QuestionsStatus.partial) {
+    return QuestionsStatus.partial;
+  } else { // a wrong, b not partial
+    return QuestionsStatus.wrong;
+  }
+}
+QuestionsStatus jointStatus(Iterable<Question> questions) {
+  return questions.map((q) => q.status()).fold(QuestionsStatus.correct, combineStatus);
+}
+
+class Question {
+  final Expression<bool> expr;
+  final List<Var> vars;
+  late final String q;  // pretty representation
+  late final String id;  // more canonical representation for database
+  List<String>? _cachedSolution;
+  final List<String> inputs = [];  // we use String instead of F because of X
+  bool isPartial;
+  static const _dottedFence = '⦙', _equiv = '≡';
+
+  Question(this.expr, this.vars, {this.isPartial = false}) {
+    final s = expr.toString();
+    q = s.replaceAll('=', _equiv).replaceAll('.', _dottedFence);
+    id = s.replaceAll(' ', '');
+    final numBlanks = '?'.allMatches(q).length;
+    assert(numBlanks == numVariables);
+  }
+
+  int get numVariables => vars.length;
+
+  QuestionsStatus status() {
+    if (inputs.length < numVariables) {
+      return QuestionsStatus.partial;
+    } else if (_cachedSolution != null && listEquals(inputs, _cachedSolution)) {
+      return QuestionsStatus.correct;
+    } else if (expr.eval(Map.fromIterables(vars, inputs.map(F.parse)))) {
+      _cachedSolution = List.unmodifiable(inputs);  // we cache a copy of the last correct solution only
+      return QuestionsStatus.correct;
+    } else {
+      return QuestionsStatus.wrong;
+    }
+  }
+
+  @override
+  toString() => 'Q($q, ${inputs.join(',')})';
+
+  String stringifyInputs() => inputs.join(';');
+  List<String> unstringifyInputs(String s) => s == '' ? [] : s.split(';');
+  String fullId(Level level) => '${level.id}:$id';
+
+  Map<String, String> toMap(Level level) {
+    return {
+      columnId: fullId(level),
+      columnLevel: level.id,
+      columnQuestion: q,
+      columnInputs: stringifyInputs(),
+    };
+  }
+
+  void updateInputs(List<String> newInputs) {
+    if (newInputs.length <= numVariables) {
+      inputs.clear();
+      inputs.addAll(newInputs);
+    }
+    // otherwise, we ignore the change to avoid inconsistencies
+  }
+}
+
+class QuestionsWithIndex {
+  final List<Question> questions;
+  int activeIndex = 0;
+  QuestionsWithIndex(this.questions);
+  Question get activeQuestion => questions[activeIndex];
+
+  Iterable<Question> _previousQuestions(int idx) sync* {
+    for (var j = idx - 1; j >= 0; j--) {
+      yield questions[j];
+    }
+  }
+
+  QuestionsStatus activeFullQuestionStatus() {
+    int idx = activeIndex;
+    while (questions[idx].isPartial) {
+      idx++;
+    }
+    final s = combineStatus(
+      questions[idx].status(),
+      jointStatus(_previousQuestions(idx).takeWhile((q) => q.isPartial)));
+    return s;
+  }
+
+  Iterable<List<MapEntry<int, Question>>> fullQuestions() sync* {
+    List<MapEntry<int, Question>> buf = [];
+    for (final e in questions.asMap().entries) {
+      buf.add(e);
+      if (!e.value.isPartial) {
+        yield buf;
+        buf = [];
+      }
+    }
+    assert(buf.isEmpty, "last question must not be partial");
+  }
+}
+
+class Level {
+  final String id;
+  final QuestionsWithIndex exercise;
+  final QuestionsWithIndex exam;
+  bool clicked = false;
+  Level(this.id, List<Question> questions, List<Question> examQuestions):
+      exercise = QuestionsWithIndex(questions),
+      exam = QuestionsWithIndex(examQuestions) {
+    exam.questions.asMap().forEach((i, q) {
+      q.isPartial = i < exam.questions.length - 1;
+    });
+  }
+
+  @override
+  toString() {
+    return 'Level(questions: [${exercise.questions.join(',')}], examQuestions: [${exam.questions.join(',')}], activeQuestion: ${exercise.activeIndex}, activeExamQuestion: ${exam.activeIndex})';
+  }
+
+  bool isSolved() => jointStatus(exam.questions) == QuestionsStatus.correct;
+}
+
+final Var<F> y = Var(), z = Var();
+final yz = dot(y, z);
+typedef Q = Question;
+Question q1(Expression<F> lhs, {bool isPartial = false}) {
+  return Question(lhs.eq(y), [y], isPartial: isPartial);
+}
+Question q2(Expression<G> lhs, {bool isPartial = false}) {
+  return Question(lhs.eq(yz), [y, z], isPartial: isPartial);
+}
+
+class Tuple<A, B> {
+  final A left;
+  final B right;
+  Tuple(this.left, this.right);
+}
+
+class Game with ChangeNotifier {
+  final List<Level> levels = [
+    Level("0", [], [q1(C(1) + C(2))]),
+    Level("1", [ // addition
+      q1(C(3) + C(4)),
+      q1(C(4) + C(3)),
+      q1(C(3) + C(7)),
+      q1(C(5) + C(7)),
+      q1(C(5) + C(8)),
+      q1(C(6) + C(6)),
+      q1(X + C(3)),
+      q1(X + C(4)),
+      q1(C(9) + C(8)),
+      q1(C(6) + X),
+    ], [
+      q1(C(7) + C(8)),
+      q1(C(1) + X),
+      q1(X + X),
+    ]),
+    Level("2", [ // subtraction
+      q1(C(6) - C(3)),
+      q1(C(0) - C(3)),
+      q1(-C(3)),
+      q1(-C(5)),
+      q1(C(7) - C(8)),
+    ], [
+      q1(X - C(7)),
+      q1(-C(1)),
+      q1(-X),
+    ]),
+    Level("3", [ // multiplication
+      q1(C(2) * C(3)), // below 11
+      q1(C(5) * C(5)), // first above 22
+      q1(C(6) * C(9)), // way larger
+      q1(C(1) * C(0)), // 1
+      q1(C(1) * X), // 1
+      q1(C(7) * C(5)),
+      q1(X * C(6)),
+    ], [
+      q1(C(7) * C(8)),
+      q1(X * C(0)),
+      q1(X * X),
+    ]),
+    Level("4", [ // division by 2
+      q1(C(4) * C(2)),
+      q1(C(8) / C(2)),
+      q1(C(6) * C(2)),
+      q1(C(1) / C(2)),
+      q1(C(3) / C(2)),
+    ], [
+      q1(C(5) / C(2)),
+      q1(C(9) / C(2)),
+      q1(X / C(2)),
+    ]),
+    Level("5", [ // division
+      q1(C(1) / C(3)),
+      q1(C(2) / C(3)),  // double of previous
+      q1(C(5) / C(4)),
+      q1(X / C(4)),  // double of previous
+      q1(C(1) / C(6)),  // denominator of exam
+    ], [
+      q1(C(1) / C(7)),
+      q1(C(1) / X),
+      q1(C(5) / C(6)),
+    ]),
+    Level("6", [ // addition
+      q2(dot(1,3) + dot(4,0)),
+      q2(dot(4,2) + dot(8,0)), // intentionally 1.2 vs 12=4+8
+      q2(dot(4,4) + dot(0,1)),
+      q2(dot(4,4) + dot(0,8)),
+      q2(dot(5,5) + dot(9,9)), // componentwise structure
+      q2(dot(7,X) + dot(X,5)),
+      q2(dot(6,7) + dot(9,7)),
+    ], [
+      q2(dot(0,X) + dot(X,X)),
+      q2(dot(5,5) + dot(8,X)),
+      q2(dot(X,6) + dot(X,6)),
+    ]),
+    Level("7", [ // multiplication (result partial 1)
+      q2(dot(2,0) * dot(4,0)),
+      q2(dot(3,0) * dot(6,0)),
+      q2(dot(8,0) * dot(8,0)),
+      Q((dot(0,1) * dot(0,1)).eq(dot(y,0)), [y]),
+      q2(dot(0,1) * dot(0,3)),
+      q2(dot(0,X) * dot(0,1)),
+      q2(dot(0,5) * dot(0,4)),
+      q2(dot(0,8) * dot(0,8)),
+    ], [
+      q2(dot(7,0) * dot(9,0)),
+      q2(dot(0,7) * dot(0,9)),
+      q2(dot(0,X) * dot(0,X)),
+    ]),
+    Level("8", [ // multiplication (result partial 2)
+      q2(dot(1,0) * dot(7,0)),
+      q2(dot(1,0) * dot(X,0)),
+      q2(dot(1,0) * dot(0,1)),
+      q2(dot(2,0) * dot(0,1)),
+      q2(dot(2,0) * dot(0,7)),
+      q2(dot(2,0) * dot(1,0)),
+      q2(dot(0,2) * dot(1,0)), // commutative
+      q2(dot(0,5) * dot(6,0)),
+      q2(dot(0,8) * dot(3,0)),
+      q2(dot(0,6) * dot(9,0)),
+    ], [
+      q2(dot(7,0) * dot(0,3)),
+      q2(dot(0,7) * dot(3,0)),
+      q2(dot(0,X) * dot(X,0)),
+    ]),
+    Level("8.1", [ // multiplication (factor partial 1)
+      q2(dot(1,0) * dot(2,0)),
+      q2(dot(1,0) * dot(0,4)),
+      q2(dot(1,0) * dot(2,4)),
+      q2(dot(2,0) * dot(2,4)),
+      q2(dot(4,0) * dot(2,4)),
+      q2(dot(7,0) * dot(1,8)),
+      q2(dot(7,3) * dot(7,0)), // commutative
+      q2(dot(2,9) * dot(2,0)),
+    ], [
+      q2(dot(6,0) * dot(3,9)),
+      q2(dot(2,8) * dot(5,0)),
+      q2(dot(7,X) * dot(X,0)),
+    ]),
+    Level("8.2", [ // multiplication (factor partial 2)
+      q2(dot(1,0) * dot(0,1)),
+      q2(dot(0,3) * dot(0,1)),
+      q2(dot(1,3) * dot(0,1)), // first complicated case
+      q2(dot(1,3) * dot(0,5)),
+      q2(dot(3,0) * dot(0,1)),
+      q2(dot(0,9) * dot(0,1)),
+      q2(dot(3,9) * dot(0,1)),
+      q2(dot(8,X) * dot(0,1)),
+      q2(dot(2,6) * dot(0,4)),
+      q2(dot(0,1) * dot(5,4)), // commutative
+      q2(dot(0,7) * dot(7,3)),
+    ], [
+      q2(dot(5,8) * dot(0,4)),
+      q2(dot(0,6) * dot(3,9)),
+      q2(dot(1,1) * dot(0,1)),
+    ]),
+    Level("9", [ // multiplication (general)
+      q2(dot(1,3) * dot(0,4)),
+      q2(dot(1,3) * dot(2,0)),
+      q2(dot(1,3) * dot(2,4)), // first general case
+      q2(dot(3,3) * dot(0,1)),
+      q2(dot(3,3) * dot(5,0)),
+      q2(dot(3,3) * dot(5,1)), // repetition
+      q2(dot(4,3) * dot(0,5), isPartial: true),
+      q2(dot(4,3) * dot(3,0), isPartial: true),
+      q2(dot(4,3) * dot(3,5)), // repetition
+      q2(dot(2,5) * dot(0,4), isPartial: true),
+      q2(dot(2,5) * dot(2,0), isPartial: true),
+      q2(dot(2,5) * dot(2,4)), // repetition
+      q2(dot(5,1) * dot(6,4)), // direct
+      q2(dot(9,1) * dot(1,9)), // direct
+    ], [
+      q2(dot(1,1) * dot(1,1)),
+      q2(dot(X,X) * dot(6,4)),
+      q2(dot(6,7) * dot(8,9)),
+    ]),
+    Level("9.1", [
+      q2(dot(0,7) * dot(0,4)),
+      q2(-dot(0,4) * dot(0,4)),
+      q2(dot(2,7) * dot(2,4)),
+      Q((dot(2,y) * dot(2,1)).eq(dot(z,0)), [y,z]), // well-defined for non-zero first component
+      Q((dot(1,y) * dot(1,3)).eq(dot(z,0)), [y,z]),
+      Q((dot(2,y) * dot(2,2)).eq(dot(z,0)), [y,z]),
+      Q((dot(5,y) * dot(5,5)).eq(dot(z,0)), [y,z]),
+    ], [
+      Q((dot(1,y) * dot(1,9)).eq(dot(z,0)), [y,z]),
+      Q((dot(3,y) * dot(3,X)).eq(dot(z,0)), [y,z]),
+      Q((dot(X,y) * dot(X,X)).eq(dot(z,0)), [y,z]),
+    ]),
+    Level("9.2", [ // division (divisor partial)
+      q2(dot(4,0) / dot(2,0)),
+      q2(dot(2,0) / dot(2,0)),
+      q2(dot(1,0) / dot(2,0)),
+      q2(dot(1,6) / dot(2,0)),
+      q2(dot(6,4) / dot(3,0)),
+      q2(dot(5,2) / dot(4,0)),
+    ], [
+      q2(dot(8,5) / dot(2,0)),
+      q2(dot(3,X) / dot(7,0)),
+      q2(dot(6,2) / dot(X,0)),
+    ]),
+    Level("10", [ // division (general)
+      Q((dot(1,y) * dot(1,1)).eq(dot(z,0)), [y,z]),
+      q2(dot(2,0) / dot(1,1)),
+      q2(dot(1,0) / dot(1,1)),
+      Q((dot(1,y) * dot(1,2)).eq(dot(z,0)), [y,z]),
+      q2(dot(1,0) / dot(1,2)), // more direct
+      Q((dot(1,y) * dot(1,3)).eq(dot(z,0)), [y,z]),
+      q2(dot(1,0) / dot(1,3)), // repetition
+      q2(dot(5,0) / dot(1,3)),
+      Q((dot(4,y) * dot(4,5)).eq(dot(z,0)), [y,z], isPartial: true),
+      q2(dot(1,0) / dot(4,5)), // repetition
+      q2(dot(2,7) / dot(4,5)), // fully general case
+      Q((dot(8,y) * dot(8,9)).eq(dot(z,0)), [y,z], isPartial: true),
+      q2(dot(1,0) / dot(8,9), isPartial: true),
+      q2(dot(2,6) / dot(8,9)), // repetition
+      q2(dot(1,0) / dot(5,4)), // direct
+      q2(dot(1,0) / dot(9,2)), // direct
+      q2(dot(2,3) / dot(4,7)), // direct
+      q2(dot(8,5) / dot(3,6)), // direct
+    ], [
+      q2(dot(1,0) / dot(2,1)),
+      q2(dot(3,1) / dot(3,X)),
+      q2(dot(5,8) / dot(0,1)),
+    ]),
+    Level("11", [ // squares
+      Q(dot(4,0).eq(dot(y,0).square()), [y]),
+      Q(dot(9,0).eq(yz.square()), [y,z]),
+      Q(dot(1,0).eq(yz.square()), [y,z]),
+      Q(dot(X,0).eq(yz.square()), [y,z]),
+    ], [
+      Q(dot(5,0).eq(yz.square()), [y,z]),
+      Q(dot(2,0).eq(yz.square()), [y,z]),
+      Q(dot(8,0).eq(yz.square()), [y,z]),
+    ]),
+  ];
+
+  final Database? db;
+  bool reset = false;
+  int _inputCount = 0;
+  int _doStatusAnimationAtCount = -1;
+  Game(this.db);
+
+  bool doStatusAnimation() {
+    return _doStatusAnimationAtCount == _inputCount;
+  }
+
+  final List<int> _activeLevelStack = [0];
+  int get activeLevel => _activeLevelStack.last;
+  set activeLevel(int level) {
+    _activeLevelStack[_activeLevelStack.length - 1] = level;
+  }
+  bool get inExamScreen => _activeLevelStack.length == 1;
+  int levelsUnlocked = 0;
+  bool get finished => levelsUnlocked >= levels.length;
+  bool get _exam1Unlocked => levelsUnlocked > 1 || levels[1].clicked || levels[1].exercise.questions.any((q) => q.inputs.isNotEmpty);
+  bool examUnlocked(int i) => i <= levelsUnlocked && (i != 1 || _exam1Unlocked) || debugUnlockAll;
+
+  Tuple<Level, Question> keyPressed(String key) {
+    final l = levels[activeLevel];
+    final q = inExamScreen ? l.exam.activeQuestion : l.exercise.activeQuestion;
+    final numBlanks = '?'.allMatches(q.q).length;
+    if (!inExamScreen || examUnlocked(activeLevel)) {
+      _inputCount++;
+      if (key == 'backspace') {
+        if (q.inputs.isNotEmpty) {
+          q.inputs.removeLast();
+        } else {
+          _movePrevious(l);
+        }
+      } else  { // ordinary key
+        if (q.inputs.length >= numBlanks) {
+          q.inputs.clear();
+        }
+        q.inputs.add(key);
+        if (q.inputs.length == numBlanks) {
+          _moveNext(l);
+        }
+      }
+    } // else this exam is not yet unlocked, so we ignore the input (relevant for exam 1 only)
+    notifyListeners();
+    return Tuple(l, q);
+  }
+
+  void _movePrevious(Level l) {
+    final qq = inExamScreen ? l.exam : l.exercise;
+    if (qq.activeIndex > 0) {
+      qq.activeIndex -= 1;
+      if (qq.activeQuestion.inputs.isNotEmpty) {
+        qq.activeQuestion.inputs.removeLast();
+      }
+    }
+  }
+
+  void _moveNext(Level l) {
+    final qq = inExamScreen ? l.exam : l.exercise;
+    final status = qq.activeFullQuestionStatus();
+    if (status == QuestionsStatus.wrong) {
+      _doStatusAnimationAtCount = _inputCount;
+    }
+    if (qq.activeIndex < qq.questions.length - 1) {
+      if (qq.activeQuestion.isPartial || status == QuestionsStatus.correct) {
+        qq.activeIndex += 1;
+      }
+    }
+    if (inExamScreen && activeLevel <= levels.length - 1 && l.isSolved()) {
+      if (activeLevel == levels.length - 1) {
+        levelsUnlocked = levels.length;  // i.e. larger than last level, signalling the game is finished
+      } else { // activeLevel < levels.length - 1
+        activeLevel += 1;
+        if (activeLevel > levelsUnlocked) {
+          levelsUnlocked = activeLevel;
+        }
+      }
+    }
+  }
+
+  void levelTapped(int questionIdx, {required bool inExam, int levelIdx = 0}) {
+    _inputCount++;
+    if (inExam) {
+      activeLevel = levelIdx;
+      levels[activeLevel].exam.activeIndex = questionIdx;
+    } else {
+      levels[activeLevel].exercise.activeIndex = questionIdx;
+    }
+    notifyListeners();
+  }
+
+  void pushLevel(int levelIdx) {
+    if (inExamScreen) {
+      _inputCount++;
+      _activeLevelStack.add(levelIdx);
+      levels[activeLevel].clicked = true;
+      // we do not notify listeners here to avoid flicker, as the screen is replaced by LevelScreen anyway
+    }
+  }
+  void popLevel() {
+    if (!inExamScreen) {
+      _inputCount++;
+      _activeLevelStack.removeLast();
+      notifyListeners(); // to notify about change of active level
+    }
+  }
+
+  Future<void> storeAnswer(Level level, Question question) async {
+    await db?.insert(tableAnswers, question.toMap(level), conflictAlgorithm: ConflictAlgorithm.replace);
+  }
+
+  Future<Map<String, String>> loadAnswers() async {
+    if (db != null) {
+      List<Map> maps = await (db!.query(tableAnswers, columns: [columnId, columnInputs]));
+      // map from fullId to stringified answer
+      return Map.fromEntries(maps.expand((m) {
+        final id = m[columnId];
+        final answer = m[columnInputs];
+        return (id == null || answer == null) ? [] : [MapEntry(id , answer)];
+      }));
+    } else {
+      return Future.value({});
+    }
+  }
+
+  Future<String?> loadKeyValue(String key) async {
+    if (db != null) {
+      List<Map> maps = await db!.query(tableKV,
+        where: '$columnKey = ?',
+        whereArgs: [key],
+      );
+      return maps.isNotEmpty ? maps.first[columnValue] : null;
+    } else {
+      return null;
+    }
+  }
+
+  Future<void> storeKeyValue(String key, String value) async {
+    if (db != null) {
+      await db!.insert(tableKV, {columnKey: key, columnValue: value}, conflictAlgorithm: ConflictAlgorithm.replace);
+    }
+  }
+
+  Future<void> recomputeExamsState() async {
+    // we store and load the id instead of the index to handle new levels
+    // inserted before the currently unlocked level
+    final levelId = await loadKeyValue(levelsUnlockedKey);
+    for (var i = 0; i < levels.length; i++) {
+      var l = levels[i];
+      // restore activeExamQuestion
+      for (var j = 0; j < l.exam.questions.length; j++) {
+        l.exam.activeIndex = j;
+        if (l.exam.activeQuestion.status() == QuestionsStatus.partial) {
+          break;
+        }
+      }
+      // restore unlocked status
+      if (l.id == levelId) {
+        levelsUnlocked = i;
+        if (i == levels.length - 1 && l.isSolved()) {
+          levelsUnlocked = levels.length;  // game is finished
+        }
+        break;
+      }
+    }
+  }
+
+  Future<void> storeLevelsUnlocked() {
+    final levelId = levels[levelsUnlocked < levels.length ? levelsUnlocked : levels.length - 1].id;
+    return storeKeyValue(levelsUnlockedKey, levelId);
+  }
+
+  Future<void> resetProgress() async {
+    levelsUnlocked = 0;
+    await storeLevelsUnlocked();
+    if (db != null) {
+      await db!.delete(tableAnswers);
+    }
+    reset = true;
+  }
+}
diff --git a/lib/main.dart b/lib/main.dart
new file mode 100644
index 0000000..2761ba0
--- /dev/null
+++ b/lib/main.dart
@@ -0,0 +1,658 @@
+import 'dart:async';
+import 'dart:convert';
+import 'dart:math';
+import 'package:flutter/material.dart';
+import 'package:flutter/foundation.dart';
+import 'package:flutter/services.dart';
+import 'package:provider/provider.dart';
+import 'package:path/path.dart';
+import 'package:sqflite/sqflite.dart';
+import 'package:package_info_plus/package_info_plus.dart';
+import 'package:everest/game.dart';
+import 'package:flex_color_scheme/flex_color_scheme.dart';
+
+const appName = 'Everest';
+const String themeModeKey = 'settings:themeMode';
+const String pureBlackKey = 'settings:pureBlack';
+
+Icon questionsStatusIcon(BuildContext context, QuestionsStatus status) {
+  final light = Theme.of(context).brightness == Brightness.light;
+  switch (status) {
+    case QuestionsStatus.partial: return Icon(Icons.circle_outlined, color: Theme.of(context).colorScheme.secondary.withOpacity(.75));
+    case QuestionsStatus.correct: return Icon(Icons.check_circle, color: Color(light ? 0xff1ca23e : 0xff2fae49));
+    case QuestionsStatus.wrong: return Icon(Icons.cancel, color: Color(light ? 0xffd51529 : 0xfff6313a));
+  }
+}
+
+class DampedCurve extends Curve {
+  // a linearly damped oscillation in reverse
+  @override double transformInternal(double t) {
+    return cos(16*(1-t))*t;
+  }
+}
+final _dampedCurve = DampedCurve();
+
+class RotateCurve extends Curve {
+  @override double transformInternal(double t) => t < 0.5 ? 0 : -cos(t*pi);
+}
+final _rotateCurve = RotateCurve();
+
+class StatusIcon extends StatefulWidget {
+  final Widget child;
+  const StatusIcon(this.child, {Key? key}) : super(key: key);
+
+  @override
+  State<StatusIcon> createState() => _StatusIconState();
+}
+
+class _StatusIconState extends State<StatusIcon>
+    with SingleTickerProviderStateMixin {
+  late final AnimationController _controller = AnimationController(
+    duration: const Duration(milliseconds: 70),
+    reverseDuration: const Duration(milliseconds: 420),
+    vsync: this,
+  );
+  late final Animation<Offset> _animation = Tween<Offset>(
+    begin: Offset.zero,
+    end: const Offset(-0.225, 0.0),
+  ).animate(CurvedAnimation(
+    parent: _controller,
+    curve: Curves.easeInOutSine,
+    reverseCurve: _dampedCurve,
+  ));
+
+  @override
+  void dispose() {
+    _controller.dispose();
+    super.dispose();
+  }
+
+  Future<void> _runAnimation() async {
+    try {  // workaround for intermediate disposal of _controller
+      _controller.reset();  // stops previous animation if still in progress
+      await _controller.forward().orCancel;
+      await _controller.reverse().orCancel;
+    } on TickerCanceled { /* ignore */ }
+  }
+
+  @override
+  Widget build(BuildContext context) {
+    _runAnimation();
+    return SlideTransition(
+      position: _animation,
+      child: widget.child,
+    );
+  }
+}
+
+class VerticalScaleTransition extends StatefulWidget {
+  final Widget child;
+  final Animation<double> animation;
+  const VerticalScaleTransition(this.child, this.animation, {Key? key}) : super(key: key);
+  @override State<VerticalScaleTransition> createState() {
+    final s = _VerticalScaleTransitionState();
+    s.scaleY = animation.value; // may be 1.0 or 0.0 depending on whether this is initial creation or animated switch, avoids flickering
+    animation.addListener(s.update);
+    return s;
+  }
+}
+class _VerticalScaleTransitionState extends State<VerticalScaleTransition> {
+  double scaleY = 1;
+  void update() => setState(() => scaleY = widget.animation.value);
+  @override Widget build(BuildContext context) => Transform.scale(scaleY: scaleY, child: widget.child);
+}
+
+Widget questionsStatusWidget(BuildContext context, QuestionsStatus status, bool animateStatusWrong) {
+  Widget icon = questionsStatusIcon(context, status);
+  if (animateStatusWrong && status == QuestionsStatus.wrong) {
+    icon = StatusIcon(icon);
+  }
+  return AnimatedSwitcher(
+    duration: const Duration(milliseconds: 330),
+    transitionBuilder: (Widget child, Animation<double> animation) => VerticalScaleTransition(child, animation),
+    switchInCurve: _rotateCurve,
+    switchOutCurve: _rotateCurve,
+    child: Container(
+      key: ValueKey<QuestionsStatus>(status),
+      child: icon,
+    ),
+  );
+}
+
+// TODO turn function into widget
+Widget questionsWidget(BuildContext context, List<Question> questions, bool isActive, int focussedQuestion, bool animateStatusWrong, {required void Function(int) onTap}) {
+  final status = jointStatus(questions);  // TODO cache this?
+  final c = Column(
+    children: Iterable.generate(questions.length).map((i) {
+      // the following is more direct than expr.str() and works since all variables appear exactly once from left to right
+      final q = questions[i].inputs.fold<String>(questions[i].q, (q, s) => q.replaceFirst('?', s));
+      Widget? t;
+      if (isActive && i == focussedQuestion) {
+        var j = q.indexOf('?');
+        if (j == -1) {
+          j = questions[i].q.indexOf('?'); // relies on all replacements being single characters
+        }
+        if (j != -1) {
+          t = Text.rich(TextSpan(
+            text: q.substring(0, j),
+            style: _biggerFont,
+            children: [
+              // TextSpan(text: q.substring(j, j+1), style: TextStyle(backgroundColor: Theme.of(context).focusColor)),
+              WidgetSpan( // with padding
+                child: Container(
+                  padding: const EdgeInsets.symmetric(horizontal: 3.0),
+                  decoration: BoxDecoration(
+                    color: Theme.of(context).focusColor,
+                    borderRadius: const BorderRadius.all(Radius.circular(3.0)),
+                  ),
+                  child: Text(q.substring(j, j+1), style: _biggerFont),
+                ),
+              ),
+              TextSpan(text: q.substring(j+1)),
+            ],
+          ));
+        }
+      }
+      t ??= Text(q, style: _biggerFont);
+      return ListTile(title: t, trailing: (i == questions.length - 1) ? questionsStatusWidget(context, status, animateStatusWrong && isActive) : null, onTap: () => onTap(i));
+    }).toList(),
+  );
+  // Here we are careful to keep the widget tree the same regardless of whether widget is active,
+  // since otherwise the status switch animation does not show.
+  return Container(color: isActive ? Theme.of(context).highlightColor : Theme.of(context).scaffoldBackgroundColor, child: c);
+}
+
+class BouncingWidget extends StatefulWidget {
+  final Widget child;
+  const BouncingWidget(this.child, {Key? key}) : super(key: key);
+
+  @override
+  State<BouncingWidget> createState() => _BouncingWidgetState();
+}
+
+class _BouncingWidgetState extends State<BouncingWidget>
+    with SingleTickerProviderStateMixin {
+  // see https://api.flutter.dev/flutter/widgets/SlideTransition-class.html
+  late final AnimationController _controller = AnimationController(
+    duration: const Duration(milliseconds: 400),
+    reverseDuration: const Duration(milliseconds: 800),
+    vsync: this,
+  );
+  late final Animation<Offset> _offsetAnimation = Tween<Offset>(
+    begin: Offset.zero,
+    end: const Offset(-1.0, 0.0),
+  ).animate(CurvedAnimation(
+    parent: _controller,
+    curve: Curves.easeInOutBack,
+    reverseCurve: Curves.bounceIn,
+  ));
+
+  // instead of a permanent long animation, we use a timer with a short animation to avoid permanent high cpu usage
+  late final Timer _timer;
+  _BouncingWidgetState() {
+    // despite the `late`, defining the timer here in the constructor (in contrast
+    // to initializing it at declaration) ensures that it is actually started
+    _timer = Timer.periodic(const Duration(seconds: 8), (timer) async {
+      await _controller.forward();
+      await _controller.reverse();
+    });
+  }
+
+  @override
+  void dispose() {
+    _timer.cancel();
+    _controller.dispose();
+    super.dispose();
+  }
+
+  @override
+  Widget build(BuildContext context) {
+    return SlideTransition(
+      position: _offsetAnimation,
+      child: widget.child,
+    );
+  }
+}
+
+Iterable<A> interleave<A>(Iterable<A> it, A separator) {
+  return it.expand((a) => [separator, a]).skip(1);
+}
+
+const listPadding = EdgeInsets.all(8.0);
+const _biggerFont = TextStyle(fontSize: 18.0);
+
+
+class Keyboard extends StatelessWidget {
+  const Keyboard({Key? key}) : super(key: key);
+
+  static const _keys = [
+    ['1', '4', '7', 'X'],
+    ['2', '5', '8', '0'],
+    ['3', '6', '9', 'backspace'],
+    // ['backspace'],
+  ];
+  static const _keyIcons = {
+    'backspace': Icons.backspace,
+  };
+
+  Widget keyButton(String label, BuildContext context) {
+    return Consumer<Game>(builder: (context, game, child) =>
+      Padding(
+        padding: const EdgeInsets.all(2),
+        child: SizedBox(
+          height: 44,
+          width: 66,
+          child: OutlinedButton(
+            child: _keyIcons.containsKey(label) ? Icon(_keyIcons[label], size: 26) : Text(label, style: const TextStyle(fontSize: 20)),
+            onPressed: () async {
+              // debugPrint('  Key $label pressed');
+              final levelQuestion = game.keyPressed(label);
+              await game.storeAnswer(levelQuestion.left, levelQuestion.right);
+              await game.storeLevelsUnlocked();
+            },
+          ),
+        ),
+      ),
+    );
+  }
+
+  @override
+  Widget build(BuildContext context) {
+    return
+      Container( // alternatively use Material(elevation..)
+        decoration: BoxDecoration(
+          color: Theme.of(context).bottomAppBarColor,
+          boxShadow: [
+            BoxShadow(color: Theme.of(context).shadowColor.withOpacity(0.4), blurRadius: 4.0, offset: const Offset(0.0, -0.75)),
+          ],
+        ),
+        child: Row(
+          mainAxisAlignment: MainAxisAlignment.center,
+          crossAxisAlignment: CrossAxisAlignment.start,
+          children: _keys.map((col) =>
+            Column(
+              mainAxisAlignment: MainAxisAlignment.center,
+              children: col.map((s) => keyButton(s, context)).toList(),
+            )
+          ).toList(),
+        ),
+    );
+  }
+}
+
+Widget withKeyboard(BuildContext context, Widget child) {
+  final cs = [child, const Hero(tag: 'thekeyboard', child: Keyboard())];
+  return MediaQuery.of(context).orientation == Orientation.landscape ? Row(children: cs) : Column(children: cs);
+}
+
+// setting thickness/color as a workaround for invisible dividers in mobile web browser https://github.com/flutter/flutter/issues/46339
+Widget divider(BuildContext context) => Divider(
+  thickness: 0.5,
+  color: Theme.of(context).colorScheme.secondary.withOpacity(0.2),
+);
+
+class LevelScreen extends StatelessWidget {
+  const LevelScreen({ Key? key }) : super(key: key);
+
+  @override
+  Widget build(BuildContext context) {
+    return Consumer2<Game, Level>(builder: (context, game, l, child) {
+      return ListView(
+        padding: listPadding,
+        children: interleave(
+          l.exercise.fullQuestions().map((es) => InkWell(
+            child: questionsWidget(context,
+              es.map((e) => e.value).toList(),
+              es[0].key <= l.exercise.activeIndex && es.last.key >= l.exercise.activeIndex,
+              l.exercise.activeIndex - es[0].key,
+              game.doStatusAnimation(),
+              onTap: (j) => game.levelTapped(es[0].key + j, inExam: false),
+            ),
+          )),
+          divider(context),
+        ).toList(),
+      );
+    });
+  }
+}
+
+class SettingsScreen extends StatelessWidget {
+  const SettingsScreen({ Key? key }) : super(key: key);
+
+  @override
+  Widget build(BuildContext context) {
+    final ThemeData theme = Theme.of(context);
+    final TextStyle textStyle = theme.textTheme.bodyText2!;
+    return ListView(
+      padding: listPadding,
+      children: [
+        const ListTile(
+          leading: Icon(Icons.settings_brightness),
+          title: Text('Theme'),
+        ),
+        Consumer2<World, Game>(builder: (context, world, game, child) =>
+          Column(
+            children: [
+              ...(ThemeMode.values.map((ThemeMode m) =>
+                RadioListTile<ThemeMode>(
+                  value: m,
+                  groupValue: world.themeMode,
+                  title: Text(m.name),
+                  onChanged: (mode) async {
+                    world.switchTheme(themeMode: m);
+                    return game.storeKeyValue(themeModeKey, m.toString());
+                  },
+                ),
+              )),
+              SwitchListTile(
+                title: const Text("Use pure black background in dark theme"),
+                subtitle: const Text("Mainly intended for OLED screens"),
+                value: world.pureBlack,
+                onChanged: (bool value) async {
+                  world.switchTheme(pureBlack: value);
+                  return game.storeKeyValue(pureBlackKey, value.toString());
+                },
+              ),
+            ],
+          ),
+        ),
+        divider(context),
+        Consumer2<World, Game>(builder: (context, world, game, child) =>
+          ListTile(
+            leading: const Icon(Icons.restore),
+            title: const Text('Restart'),
+            subtitle: const Text('Long press to reset the progress.'),
+            onLongPress: () async {
+              await game.resetProgress();
+              world.resetWorld();
+            },
+          ),
+        ),
+        divider(context),
+        AboutListTile(
+          icon: const Icon(Icons.info_outline),
+          applicationVersion: "Version ${Provider.of<World>(context).appInfo.version}",
+          aboutBoxChildren: [
+            SelectableText.rich(
+              TextSpan(
+                children: <TextSpan>[
+                  TextSpan(style: textStyle, text: 'More info at '),
+                  TextSpan(
+                      style: textStyle.copyWith(color: theme.colorScheme.primary),
+                      text: 'https://mwageringel.github.io/everest/'),  // TODO make hyperlink clickable or copy to clipboard
+                  TextSpan(style: textStyle, text: '.'),
+                ],
+              ),
+            ),
+          ],
+        ),
+        divider(context),
+      ],
+    );
+  }
+}
+
+class ExamsScreen extends StatelessWidget {
+  const ExamsScreen({ Key? key }) : super(key: key);
+
+  void _pushExercises(BuildContext context, String title, Game game, int levelIdx) {
+    game.pushLevel(levelIdx);
+    final Level level = game.levels[levelIdx];
+    Navigator.of(context).push(
+      MaterialPageRoute<void>(
+        builder: (context) {
+          assert(game.activeLevel == levelIdx);
+          return Scaffold(
+            appBar: AppBar(
+              title: Text(title),
+            ),
+            body: withKeyboard(context, Expanded(
+              // Rather than obtaining the current level from game.activeLevel, we provide it directly,
+              // since activeLevel can change on popLevel which would cause some flickering
+              // (i.e. exercises from a different level getting rendered).
+              child: Provider<Level>.value(
+                value: level,
+                child: const LevelScreen(),
+              ),
+            )),
+          );
+        },
+      ),
+    ).then((_) {
+      game.popLevel();
+    });
+  }
+
+  void _pushSettings(BuildContext context) {
+    Navigator.of(context).push(
+      MaterialPageRoute<void>(
+        builder: (context) {
+          return Scaffold(
+            appBar: AppBar(
+              title: const Text('Settings'),
+            ),
+            body: const SettingsScreen(),
+          );
+        },
+      ),
+    );
+  }
+
+  @override
+  Widget build(BuildContext context) {
+    final scaf = Scaffold(
+      appBar: AppBar(
+        title: const Text(appName),
+        actions: [
+          IconButton(
+            icon: const Icon(Icons.menu),
+            onPressed: () => _pushSettings(context),
+            tooltip: 'Settings',
+          ),
+        ],
+      ),
+      body: withKeyboard(context, Expanded(
+        child: Consumer<Game>(builder: (context, game, child) {  // TODO too large widget?
+          return ListView.builder(
+            padding: listPadding,
+            itemCount: game.levels.length,
+            itemBuilder: (context, levelIdx) {
+              assert((levelIdx > 0) ^ game.levels[levelIdx].exercise.questions.isEmpty);
+              final level = game.levels[levelIdx];
+              final label = 'Level $levelIdx';
+              final unlocked = levelIdx <= game.levelsUnlocked || debugUnlockAll;
+              return Material( // fixes hover artifact near keyboard
+                color: Theme.of(context).scaffoldBackgroundColor,
+                child: Column(
+                  children: [
+                    if (levelIdx > 0) divider(context),
+                    if (levelIdx > 0) ListTile(
+                      title: Text(label, style: _biggerFont),
+                      trailing: levelIdx == game.levelsUnlocked && !game.levels[levelIdx].clicked
+                        ? BouncingWidget(Icon(Icons.adaptive.arrow_forward))
+                        : Icon(unlocked ? Icons.adaptive.arrow_forward : Icons.lock),
+                      enabled: unlocked,
+                      onTap: () {
+                        if (levelIdx <= game.levelsUnlocked || debugUnlockAll) {
+                          _pushExercises(context, label, game, levelIdx);
+                        }
+                      },
+                    ),
+                    if (game.examUnlocked(levelIdx) || debugUnlockAll) ...[
+                      if (levelIdx > 0) divider(context),
+                      InkWell(
+                        child: questionsWidget(context, level.exam.questions, levelIdx == game.activeLevel, level.exam.activeIndex,
+                            game.doStatusAnimation(),
+                            onTap: (i) => game.levelTapped(i, inExam: true, levelIdx: levelIdx)),
+                      ),
+                    ],
+                    if (levelIdx == game.levels.length-1 && game.finished) ListTile(
+                      title: Text('Congratulations!', style: _biggerFont.merge(TextStyle(color: Theme.of(context).colorScheme.primary))),
+                      subtitle: Text(utf8.decode(base64.decode(
+                        'T3V0c3RhbmRpbmcgYWNjb21wbGlzaG1lbnQhIFlvdSBoYXZlIGV4cGxvcmVkIHRoZSBhcml0aG1ldGlj'
+                        'cyBvZiB0aGUgZmluaXRlIGZpZWxkcyB3aXRoIDExIGFuZCAxMjEgZWxlbWVudHMuIChEaWQgeW91IG5v'
+                        'dGljZSBhIHNpbWlsYXJpdHkgd2l0aCBjb21wbGV4IG51bWJlcnM/KQ=='))),
+                      leading: const Icon(Icons.sentiment_very_satisfied),
+                    ),
+                  ],
+                ),
+              );
+            },
+          );
+        }),
+      )),
+    );
+    return Consumer<Game>(builder: (context, game, child) =>
+      WillPopScope(
+        onWillPop: () => (
+          // this asks for confirmation at back button press to avoid loss of state, when no database is available on web version
+          game.db != null ? Future.value(true) : showDialog<bool?>(
+            context: context,
+            builder: (context) => AlertDialog(
+              title: const Text('Saving not available.'),
+              content: const Text('All progress will be lost if you exit. Continue?'),
+              actions: [
+                ElevatedButton(child: const Text('Cancel'), onPressed: () => Navigator.of(context).pop(false)),
+                OutlinedButton(child: const Text('OK'), onPressed: () => Navigator.of(context).pop(true)),
+              ],
+            ),
+          ).then((x) => x ?? false)
+        ),
+        child: scaf,
+      )
+    );
+
+  }
+}
+
+class MyApp extends StatelessWidget {
+  const MyApp({Key? key}) : super(key: key);
+
+  @override
+  Widget build(BuildContext context) {
+    return Consumer<World>(builder: (context, world, child) =>
+      MaterialApp(
+        title: appName,
+        themeMode: world.themeMode,
+        theme: FlexThemeData.light(
+          fontFamily: 'NotoSansMath',
+          scheme: FlexScheme.materialBaseline,
+          primary: Colors.indigo,
+          surfaceMode: FlexSurfaceMode.highScaffoldLowSurface,
+          blendLevel: 4,
+          appBarOpacity: 0.95,
+          subThemesData: const FlexSubThemesData(
+            blendOnLevel: 4,
+            blendOnColors: false,
+          ),
+          visualDensity: FlexColorScheme.comfortablePlatformDensity,
+        ),
+        darkTheme: FlexThemeData.dark(
+          fontFamily: 'NotoSansMath',
+          scheme: FlexScheme.materialBaseline,
+          primary: Colors.indigoAccent,  // better contrast against dark background
+          surfaceMode: FlexSurfaceMode.highScaffoldLowSurface,
+          blendLevel: 10,
+          appBarStyle: FlexAppBarStyle.background,
+          appBarOpacity: 0.90,
+          subThemesData: const FlexSubThemesData(
+            blendOnLevel: 10,
+          ),
+          visualDensity: FlexColorScheme.comfortablePlatformDensity,
+          darkIsTrueBlack: world.pureBlack,
+        ),
+        home: const ExamsScreen(),
+      ),
+    );
+  }
+}
+
+// wrapper around game state in order to be able to reset the progress
+class World with ChangeNotifier {
+  ThemeMode themeMode;
+  bool pureBlack;
+  final PackageInfo appInfo;
+  World(this.appInfo, this.themeMode, this.pureBlack);
+
+  void resetWorld() {
+    notifyListeners();  // results in new game getting initialized from database
+  }
+
+  void switchTheme({ThemeMode? themeMode, bool? pureBlack}) {
+    this.themeMode = themeMode ?? this.themeMode;
+    this.pureBlack = pureBlack ?? this.pureBlack;
+    notifyListeners();
+  }
+}
+
+
+void main() async {
+  WidgetsFlutterBinding.ensureInitialized(); // Avoid errors caused by flutter upgrade.
+  Database? db;
+  try {
+    db = await openDatabase(
+      join(await getDatabasesPath(), 'everest-data.db'),
+      onCreate: (db, version) async {
+        // note that adding additional tables to existing database file requires some extra steps
+        await db.execute(
+          'CREATE TABLE $tableKV($columnKey TEXT PRIMARY KEY, $columnValue TEXT)',
+        );
+        await db.execute(
+          'CREATE TABLE $tableAnswers($columnId TEXT PRIMARY KEY, $columnLevel TEXT, $columnQuestion TEXT, $columnInputs TEXT)',
+        );
+      },
+      version: 1,
+    );
+  } on MissingPluginException {
+    db = null;  // database is not available for the web
+  }
+
+  LicenseRegistry.addLicense(() async* {
+    final license = await rootBundle.loadString('fonts/OFL.txt');
+    yield LicenseEntryWithLineBreaks(['NotoSansMath'], license);
+  });
+
+  Future<void> loadGameState(Game game) async {
+    // initialization of state from database
+    final answers = await game.loadAnswers();
+    for (final level in game.levels) {
+      for (final question in level.exercise.questions.followedBy(level.exam.questions)) {
+        final answer = answers[question.fullId(level)];
+        if (answer != null) {
+          question.updateInputs(question.unstringifyInputs(answer));
+        }
+      }
+    }
+    await game.recomputeExamsState();
+  }
+
+  Future<ThemeMode> loadThemeMode(Game game) async {
+    String? mode = await game.loadKeyValue(themeModeKey);
+    return ThemeMode.values.firstWhere((m) => m.toString() == mode, orElse: () => ThemeMode.system);
+  }
+
+  final game0 = Game(db);
+  await loadGameState(game0);  // loaded here since `create` is not asynchronous
+  final themeMode0 = await loadThemeMode(game0);
+  final pureBlack0 = (await game0.loadKeyValue(pureBlackKey)) == true.toString();  // false by default
+  final appInfo = await PackageInfo.fromPlatform();
+  runApp(
+    MultiProvider(
+      providers: [
+        ChangeNotifierProvider(create: (context) => World(appInfo, themeMode0, pureBlack0)),
+        ChangeNotifierProxyProvider<World, Game>(
+          create: (context) => game0,  // TODO avoid external variable
+          update: (context, world, game) {
+            // debugPrint(">>> update of world");
+            if (game == null || game.reset) {
+              return Game(db);  // a new game without loading state from database
+            } else {
+              return game;
+            }
+          },
+        ),
+      ],
+      child: const MyApp(),
+    ),
+  );
+}
diff --git a/pubspec.lock b/pubspec.lock
new file mode 100644
index 0000000..3cbbd31
--- /dev/null
+++ b/pubspec.lock
@@ -0,0 +1,544 @@
+# Generated by pub
+# See https://dart.dev/tools/pub/glossary#lockfile
+packages:
+  _fe_analyzer_shared:
+    dependency: transitive
+    description:
+      name: _fe_analyzer_shared
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "41.0.0"
+  analyzer:
+    dependency: transitive
+    description:
+      name: analyzer
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "4.2.0"
+  archive:
+    dependency: transitive
+    description:
+      name: archive
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "3.3.0"
+  args:
+    dependency: transitive
+    description:
+      name: args
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "2.3.1"
+  async:
+    dependency: transitive
+    description:
+      name: async
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "2.8.2"
+  boolean_selector:
+    dependency: transitive
+    description:
+      name: boolean_selector
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "2.1.0"
+  characters:
+    dependency: transitive
+    description:
+      name: characters
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.2.0"
+  charcode:
+    dependency: transitive
+    description:
+      name: charcode
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.3.1"
+  clock:
+    dependency: transitive
+    description:
+      name: clock
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.1.0"
+  collection:
+    dependency: transitive
+    description:
+      name: collection
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.16.0"
+  convert:
+    dependency: transitive
+    description:
+      name: convert
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "3.0.2"
+  coverage:
+    dependency: transitive
+    description:
+      name: coverage
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.3.2"
+  crypto:
+    dependency: transitive
+    description:
+      name: crypto
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "3.0.2"
+  fake_async:
+    dependency: transitive
+    description:
+      name: fake_async
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.3.0"
+  ffi:
+    dependency: transitive
+    description:
+      name: ffi
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.2.1"
+  file:
+    dependency: transitive
+    description:
+      name: file
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "6.1.2"
+  flex_color_scheme:
+    dependency: "direct main"
+    description:
+      name: flex_color_scheme
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "5.1.0"
+  flutter:
+    dependency: "direct main"
+    description: flutter
+    source: sdk
+    version: "0.0.0"
+  flutter_launcher_icons:
+    dependency: "direct dev"
+    description:
+      name: flutter_launcher_icons
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "0.9.3"
+  flutter_lints:
+    dependency: "direct dev"
+    description:
+      name: flutter_lints
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "2.0.1"
+  flutter_test:
+    dependency: "direct dev"
+    description: flutter
+    source: sdk
+    version: "0.0.0"
+  flutter_web_plugins:
+    dependency: transitive
+    description: flutter
+    source: sdk
+    version: "0.0.0"
+  frontend_server_client:
+    dependency: transitive
+    description:
+      name: frontend_server_client
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "2.1.3"
+  glob:
+    dependency: transitive
+    description:
+      name: glob
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "2.1.0"
+  http:
+    dependency: transitive
+    description:
+      name: http
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "0.13.4"
+  http_multi_server:
+    dependency: transitive
+    description:
+      name: http_multi_server
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "3.2.1"
+  http_parser:
+    dependency: transitive
+    description:
+      name: http_parser
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "4.0.1"
+  image:
+    dependency: transitive
+    description:
+      name: image
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "3.2.0"
+  io:
+    dependency: transitive
+    description:
+      name: io
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.0.3"
+  js:
+    dependency: transitive
+    description:
+      name: js
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "0.6.4"
+  lints:
+    dependency: transitive
+    description:
+      name: lints
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "2.0.0"
+  logging:
+    dependency: transitive
+    description:
+      name: logging
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.0.2"
+  matcher:
+    dependency: transitive
+    description:
+      name: matcher
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "0.12.11"
+  material_color_utilities:
+    dependency: transitive
+    description:
+      name: material_color_utilities
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "0.1.4"
+  meta:
+    dependency: transitive
+    description:
+      name: meta
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.7.0"
+  mime:
+    dependency: transitive
+    description:
+      name: mime
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.0.2"
+  nested:
+    dependency: transitive
+    description:
+      name: nested
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.0.0"
+  node_preamble:
+    dependency: transitive
+    description:
+      name: node_preamble
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "2.0.1"
+  package_config:
+    dependency: transitive
+    description:
+      name: package_config
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "2.1.0"
+  package_info_plus:
+    dependency: "direct main"
+    description:
+      name: package_info_plus
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.4.2"
+  package_info_plus_linux:
+    dependency: transitive
+    description:
+      name: package_info_plus_linux
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.0.5"
+  package_info_plus_macos:
+    dependency: transitive
+    description:
+      name: package_info_plus_macos
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.3.0"
+  package_info_plus_platform_interface:
+    dependency: transitive
+    description:
+      name: package_info_plus_platform_interface
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.0.2"
+  package_info_plus_web:
+    dependency: transitive
+    description:
+      name: package_info_plus_web
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.0.5"
+  package_info_plus_windows:
+    dependency: transitive
+    description:
+      name: package_info_plus_windows
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.0.5"
+  path:
+    dependency: "direct main"
+    description:
+      name: path
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.8.1"
+  petitparser:
+    dependency: transitive
+    description:
+      name: petitparser
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "5.0.0"
+  plugin_platform_interface:
+    dependency: transitive
+    description:
+      name: plugin_platform_interface
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "2.1.2"
+  pool:
+    dependency: transitive
+    description:
+      name: pool
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.5.1"
+  provider:
+    dependency: "direct main"
+    description:
+      name: provider
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "6.0.3"
+  pub_semver:
+    dependency: transitive
+    description:
+      name: pub_semver
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "2.1.1"
+  shelf:
+    dependency: transitive
+    description:
+      name: shelf
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.3.1"
+  shelf_packages_handler:
+    dependency: transitive
+    description:
+      name: shelf_packages_handler
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "3.0.1"
+  shelf_static:
+    dependency: transitive
+    description:
+      name: shelf_static
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.1.1"
+  shelf_web_socket:
+    dependency: transitive
+    description:
+      name: shelf_web_socket
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.0.2"
+  sky_engine:
+    dependency: transitive
+    description: flutter
+    source: sdk
+    version: "0.0.99"
+  source_map_stack_trace:
+    dependency: transitive
+    description:
+      name: source_map_stack_trace
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "2.1.0"
+  source_maps:
+    dependency: transitive
+    description:
+      name: source_maps
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "0.10.10"
+  source_span:
+    dependency: transitive
+    description:
+      name: source_span
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.8.2"
+  sqflite:
+    dependency: "direct main"
+    description:
+      name: sqflite
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "2.0.2+1"
+  sqflite_common:
+    dependency: transitive
+    description:
+      name: sqflite_common
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "2.2.1+1"
+  stack_trace:
+    dependency: transitive
+    description:
+      name: stack_trace
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.10.0"
+  stream_channel:
+    dependency: transitive
+    description:
+      name: stream_channel
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "2.1.0"
+  string_scanner:
+    dependency: transitive
+    description:
+      name: string_scanner
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.1.0"
+  synchronized:
+    dependency: transitive
+    description:
+      name: synchronized
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "3.0.0+2"
+  term_glyph:
+    dependency: transitive
+    description:
+      name: term_glyph
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.2.0"
+  test:
+    dependency: "direct dev"
+    description:
+      name: test
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.21.1"
+  test_api:
+    dependency: transitive
+    description:
+      name: test_api
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "0.4.9"
+  test_core:
+    dependency: transitive
+    description:
+      name: test_core
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "0.4.13"
+  typed_data:
+    dependency: transitive
+    description:
+      name: typed_data
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.3.1"
+  vector_math:
+    dependency: transitive
+    description:
+      name: vector_math
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "2.1.2"
+  vm_service:
+    dependency: transitive
+    description:
+      name: vm_service
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "8.3.0"
+  watcher:
+    dependency: transitive
+    description:
+      name: watcher
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.0.1"
+  web_socket_channel:
+    dependency: transitive
+    description:
+      name: web_socket_channel
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "2.2.0"
+  webkit_inspection_protocol:
+    dependency: transitive
+    description:
+      name: webkit_inspection_protocol
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "1.1.0"
+  win32:
+    dependency: transitive
+    description:
+      name: win32
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "2.6.1"
+  xml:
+    dependency: transitive
+    description:
+      name: xml
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "6.1.0"
+  yaml:
+    dependency: transitive
+    description:
+      name: yaml
+      url: "https://pub.dartlang.org"
+    source: hosted
+    version: "3.1.1"
+sdks:
+  dart: ">=2.17.0 <3.0.0"
+  flutter: ">=3.0.0"
diff --git a/pubspec.yaml b/pubspec.yaml
new file mode 100644
index 0000000..718984d
--- /dev/null
+++ b/pubspec.yaml
@@ -0,0 +1,109 @@
+name: everest
+description: A mathematical puzzle game.
+
+# The following line prevents the package from being accidentally published to
+# pub.dev using `flutter pub publish`. This is preferred for private packages.
+publish_to: 'none' # Remove this line if you wish to publish to pub.dev
+
+# The following defines the version and build number for your application.
+# A version number is three numbers separated by dots, like 1.2.43
+# followed by an optional build number separated by a +.
+# Both the version and the builder number may be overridden in flutter
+# build by specifying --build-name and --build-number, respectively.
+# In Android, build-name is used as versionName while build-number used as versionCode.
+# Read more about Android versioning at https://developer.android.com/studio/publish/versioning
+# In iOS, build-name is used as CFBundleShortVersionString while build-number used as CFBundleVersion.
+# Read more about iOS versioning at
+# https://developer.apple.com/library/archive/documentation/General/Reference/InfoPlistKeyReference/Articles/CoreFoundationKeys.html
+version: 1.1.0+9
+
+environment:
+  sdk: ">=2.16.2 <3.0.0"
+
+# Dependencies specify other packages that your package needs in order to work.
+# To automatically upgrade your package dependencies to the latest versions
+# consider running `flutter pub upgrade --major-versions`. Alternatively,
+# dependencies can be manually updated by changing the version numbers below to
+# the latest version available on pub.dev. To see which dependencies have newer
+# versions available, run `flutter pub outdated`.
+dependencies:
+  flutter:
+    sdk: flutter
+  sqflite:
+  path:
+
+  # The following adds the Cupertino Icons font to your application.
+  # Use with the CupertinoIcons class for iOS style icons.
+  # cupertino_icons: ^1.0.2  # TODO
+  provider: ^6.0.2
+  package_info_plus: ^1.4.2
+  flex_color_scheme: ^5.1.0
+  # scrollable_positioned_list: ^0.2.3
+
+dev_dependencies:
+  flutter_test:
+    sdk: flutter
+
+  # The "flutter_lints" package below contains a set of recommended lints to
+  # encourage good coding practices. The lint set provided by the package is
+  # activated in the `analysis_options.yaml` file located at the root of your
+  # package. See that file for information about deactivating specific lint
+  # rules and activating additional ones.
+  flutter_lints: ^2.0.1
+  test: ^1.21.1
+  flutter_launcher_icons: ^0.9.3
+
+# For information on the generic Dart part of this file, see the
+# following page: https://dart.dev/tools/pub/pubspec
+
+# The following section is specific to Flutter.
+flutter:
+
+  # The following line ensures that the Material Icons font is
+  # included with your application, so that you can use the icons in
+  # the material Icons class.
+  uses-material-design: true
+
+  # To add assets to your application, add an assets section, like this:
+  # assets:
+  #   - images/a_dot_burr.jpeg
+  #   - images/a_dot_ham.jpeg
+
+  # An image asset can refer to one or more resolution-specific "variants", see
+  # https://flutter.dev/assets-and-images/#resolution-aware.
+
+  # For details regarding adding assets from package dependencies, see
+  # https://flutter.dev/assets-and-images/#from-packages
+
+  # To add custom fonts to your application, add a fonts section here,
+  # in this "flutter" section. Each entry in this list should have a
+  # "family" key with the font family name, and a "fonts" key with a
+  # list giving the asset and other descriptors for the font. For
+  # example:
+  # fonts:
+  #   - family: Schyler
+  #     fonts:
+  #       - asset: fonts/Schyler-Regular.ttf
+  #       - asset: fonts/Schyler-Italic.ttf
+  #         style: italic
+  #   - family: Trajan Pro
+  #     fonts:
+  #       - asset: fonts/TrajanPro.ttf
+  #       - asset: fonts/TrajanPro_Bold.ttf
+  #         weight: 700
+  #
+  # For details regarding fonts from package dependencies,
+  # see https://flutter.dev/custom-fonts/#from-packages
+  fonts:
+    - family: NotoSansMath
+      fonts:
+        - asset: fonts/NotoSansMath-Regular.ttf
+
+  assets:
+    # license for NotoSansMath
+    - fonts/OFL.txt
+
+flutter_icons:
+  android: true
+  ios: false
+  image_path: assets/launcher_icon.png
diff --git a/test/expressions_test.dart b/test/expressions_test.dart
new file mode 100644
index 0000000..8fa0342
--- /dev/null
+++ b/test/expressions_test.dart
@@ -0,0 +1,71 @@
+import 'package:test/test.dart';
+import 'package:everest/expressions.dart';
+
+void main() {
+  test('addition', () {
+    final e = Con(3) + Con(7) + Con(100);
+    expect(e.toString(), equals('3 + 7 + 100'));
+    expect(e.eval({}), equals(110));
+    expect(e.eq(Con(110)).str({}), equals('3 + 7 + 100 = 110'));
+  });
+
+  test('various expression operations', () {
+    final e = -Con(3.0) * Con(4.0) + Con(14.0) / Con(7.0) - Con(1.0) + Con(3.0).square();
+    expect(e.toString(), equals('-3.0 * 4.0 + 14.0 / 7.0 - 1.0 + 3.0²'));
+    expect(e.eval({}), equals(-2.0));
+  });
+
+  test('variables', () {
+    Var<int> y = Var(), z = Var();
+    final e = Con(3) + Con(4) * y + z;
+    final vars = {y: 2, z: 5};
+    expect(e.toString(), equals('3 + 4 * ? + ?'));
+    expect(e.str(vars), equals('3 + 4 * 2 + 5'));
+    expect(e.str({z: 2, y: 5}), equals('3 + 4 * 5 + 2'));
+    expect(e.eval(vars), equals(16));
+    expect(() => e.eval({}), throwsA(isA<UnsupportedError>()));
+  });
+
+  test('eq', () {
+    final e = Con(G.F(2,3)) * Con(G.F(2,5)) * Con(G.F(6,4)) * Con(G.F(1,5));
+    expect(e.eq(Con(G.F(1,2))).eval({}), equals(true));
+    expect(e.eq(Con(G.F(5,8))).eval({}), equals(false));
+    expect(e.eq(Con(G.F(6,7))).eval({}), equals(false));
+    expect(e.eq(Con(G.F(0,0))).eval({}), equals(false));
+    expect(e.eq(Con(G.F(1,0))).eval({}), equals(false));
+    expect(e.eq(Con(G.F(0,1))).eval({}), equals(false));
+  });
+
+  final testElems = [G.F(1,2), G.F(3,4), G.F(5,7), G.F(9,2)];
+
+  test('pow', () {
+    for (final dynamic a in testElems.cast<dynamic>().followedBy([F(3), F(4)])) {
+      for (final n in [1,2,3,4,5,6,7,8,9,10]) {
+        expect(a.pow(n), equals(List.filled(n-1, a).fold(a, (dynamic b, c) => b * c)));
+      }
+    }
+  });
+
+  test('div', () {
+    for (final a in testElems) {
+      expect(a / a, equals(G.F(1,0)));
+    }
+    for (final a in [F(3), F(4), F(5), F(6)]) {
+      expect(a / a, equals(F(1)));
+    }
+  });
+
+  test('operations on G', () {
+    expect(-G.F(1,2) + G.F(3,4) * G.F(5,6) / G.F(7,8) - G.F(9,10).pow(2), equals(G.F(-1,6)));
+  });
+
+  test('dot', () {
+    expect((dot(3,4) * dot(5,8) * dot(6,5) * dot(7,X)).eq(dot(4, 2)).eval({}), equals(true));
+  });
+
+  test('parse', () {
+    expect(F.parse('X'), equals(X.eval({})));
+    expect(F.parse('-1'), equals(F(-1)));
+    expect(F.parse('123'), equals(F(123)));
+  });
+}
diff --git a/web/index.html b/web/index.html
new file mode 100644
index 0000000..ab4213d
--- /dev/null
+++ b/web/index.html
@@ -0,0 +1,107 @@
+<!DOCTYPE html>
+<html>
+<head>
+  <!--
+    If you are serving your web app in a path other than the root, change the
+    href value below to reflect the base path you are serving from.
+
+    The path provided below has to start and end with a slash "/" in order for
+    it to work correctly.
+
+    For more details:
+    * https://developer.mozilla.org/en-US/docs/Web/HTML/Element/base
+
+    This is a placeholder for base href that will be replaced by the value of
+    the `--base-href` argument provided to `flutter build`.
+  -->
+  <base href="$FLUTTER_BASE_HREF">
+
+  <meta charset="UTF-8">
+  <meta content="IE=Edge" http-equiv="X-UA-Compatible">
+  <meta name="description" content="A mathematical puzzle game.">
+
+  <!-- important so that "forced" dark mode is not applied by informing the browser about our dark mode -->
+  <meta name="color-scheme" content="dark light">
+
+  <!-- iOS meta tags & icons -->
+  <meta name="apple-mobile-web-app-capable" content="yes">
+  <meta name="apple-mobile-web-app-status-bar-style" content="black">
+  <meta name="apple-mobile-web-app-title" content="Everest">
+  <link rel="apple-touch-icon" href="icons/Icon-192.png">
+
+  <!-- Favicon -->
+  <link rel="icon" type="image/x-icon" href="favicon.ico"/>
+
+  <title>Everest</title>
+  <link rel="manifest" href="manifest.json">
+</head>
+<body>
+  <!-- This script installs service_worker.js to provide PWA functionality to
+       application. For more information, see:
+       https://developers.google.com/web/fundamentals/primers/service-workers -->
+  <script>
+    var serviceWorkerVersion = null;
+    var scriptLoaded = false;
+    function loadMainDartJs() {
+      if (scriptLoaded) {
+        return;
+      }
+      scriptLoaded = true;
+      var scriptTag = document.createElement('script');
+      scriptTag.src = 'main.dart.js';
+      scriptTag.type = 'application/javascript';
+      document.body.append(scriptTag);
+    }
+
+    if ('serviceWorker' in navigator) {
+      // Service workers are supported. Use them.
+      window.addEventListener('load', function () {
+        // Wait for registration to finish before dropping the <script> tag.
+        // Otherwise, the browser will load the script multiple times,
+        // potentially different versions.
+        var serviceWorkerUrl = 'flutter_service_worker.js?v=' + serviceWorkerVersion;
+        navigator.serviceWorker.register(serviceWorkerUrl)
+          .then((reg) => {
+            function waitForActivation(serviceWorker) {
+              serviceWorker.addEventListener('statechange', () => {
+                if (serviceWorker.state == 'activated') {
+                  console.log('Installed new service worker.');
+                  loadMainDartJs();
+                }
+              });
+            }
+            if (!reg.active && (reg.installing || reg.waiting)) {
+              // No active web worker and we have installed or are installing
+              // one for the first time. Simply wait for it to activate.
+              waitForActivation(reg.installing || reg.waiting);
+            } else if (!reg.active.scriptURL.endsWith(serviceWorkerVersion)) {
+              // When the app updates the serviceWorkerVersion changes, so we
+              // need to ask the service worker to update.
+              console.log('New service worker available.');
+              reg.update();
+              waitForActivation(reg.installing);
+            } else {
+              // Existing service worker is still good.
+              console.log('Loading app from service worker.');
+              loadMainDartJs();
+            }
+          });
+
+        // If service worker doesn't succeed in a reasonable amount of time,
+        // fallback to plaint <script> tag.
+        setTimeout(() => {
+          if (!scriptLoaded) {
+            console.warn(
+              'Failed to load app from service worker. Falling back to plain <script> tag.',
+            );
+            loadMainDartJs();
+          }
+        }, 4000);
+      });
+    } else {
+      // Service workers not supported. Just drop the <script> tag.
+      loadMainDartJs();
+    }
+  </script>
+</body>
+</html>
diff --git a/web/manifest.json b/web/manifest.json
new file mode 100644
index 0000000..20a155d
--- /dev/null
+++ b/web/manifest.json
@@ -0,0 +1,35 @@
+{
+    "name": "everest",
+    "short_name": "everest",
+    "start_url": ".",
+    "display": "standalone",
+    "background_color": "#0175C2",
+    "theme_color": "#0175C2",
+    "description": "A mathematical puzzle game.",
+    "orientation": "portrait-primary",
+    "prefer_related_applications": false,
+    "icons": [
+        {
+            "src": "icons/Icon-192.png",
+            "sizes": "192x192",
+            "type": "image/png"
+        },
+        {
+            "src": "icons/Icon-512.png",
+            "sizes": "512x512",
+            "type": "image/png"
+        },
+        {
+            "src": "icons/Icon-maskable-192.png",
+            "sizes": "192x192",
+            "type": "image/png",
+            "purpose": "maskable"
+        },
+        {
+            "src": "icons/Icon-maskable-512.png",
+            "sizes": "512x512",
+            "type": "image/png",
+            "purpose": "maskable"
+        }
+    ]
+}
diff --git a/website/index.html b/website/index.html
new file mode 100644
index 0000000..2f4b5d6
--- /dev/null
+++ b/website/index.html
@@ -0,0 +1,80 @@
+<!DOCTYPE html>
+<html lang="en">
+<head>
+<title>Everest</title>
+<meta charset="UTF-8">
+<meta name="viewport" content="width=device-width, initial-scale=1">
+<link rel="stylesheet" href="https://www.w3schools.com/w3css/4/w3.css">
+<link rel="stylesheet" href="https://fonts.googleapis.com/css?family=Noto+Sans">
+<link rel="stylesheet" href="https://fonts.googleapis.com/css?family=Montserrat">
+<style>
+body,h1,h2,h3,h4,h5,h6 {font-family: "Noto Sans", sans-serif}
+.w3-bar,h1,button {font-family: "Montserrat", sans-serif}
+.w3-content {max-width: 720px}
+</style>
+</head>
+<body>
+
+<!-- header -->
+<header class="w3-container w3-indigo w3-center" style="padding:16px 16px 16px 16px">
+  <h1 class="w3-margin w3-jumbo">Everest</h1>
+  <p class="w3-xlarge">A mathematical puzzle game</p>
+</header>
+
+<!-- first section -->
+<div class="w3-content w3-container w3-padding-48">
+  <div class="w3-row-padding w3-stretch">
+
+    <div class="w3-col m6 w3-padding-16">
+      <h1>Android App</h1>
+      <p class="w3-text-grey">
+        Recommended if you have an Android device (with Android 4.1 or above).
+      </p>
+      <!-- TODO update download url -->
+      <a href="#" class="w3-button w3-indigo w3-padding-large w3-margin-top">Download .apk file (18 MB)</a>
+    </div>
+
+    <div class="w3-col m6 w3-padding-16">
+      <h1>Browser Demo</h1>
+      <p class="w3-text-grey">
+        The web version does not support saving the progress.
+        Its layout works best with mobile devices or small browser windows.
+      </p>
+      <a href="demo/" class="w3-button w3-indigo w3-padding-large w3-margin-top">Open demo page (8 MB)</a>
+    </div>
+  </div>
+</div>
+
+<!-- second section -->
+<div class="w3-light-grey">
+  <div class="w3-content w3-padding-64 w3-container">
+    <h1>About the Game</h1>
+    <p class="w3-text-grey">
+      No mathematical knowledge is required beyond basic arithmetics.
+      All the rules of the game are found through exploration,
+      based on the concept of discovery learning.
+    </p>
+    <p class="w3-text-grey">
+      The game is free and fully open source – available on <a href="https://github.com/mwageringel/everest">GitHub</a>.
+      <a href="https://github.com/mwageringel/everest">
+        <i class="w3-hover-opacity w3-padding-small">
+          <svg stroke="currentColor" fill="currentColor" stroke-width="0" viewBox="0 0 16 16" width="20px" height="20px">
+            <path fill-rule="evenodd" d="M8 0C3.58 0 0 3.58 0 8c0 3.54 2.29 6.53 5.47 7.59.4.07.55-.17.55-.38 0-.19-.01-.82-.01-1.49-2.01.37-2.53-.49-2.69-.94-.09-.23-.48-.94-.82-1.13-.28-.15-.68-.52-.01-.53.63-.01 1.08.58 1.23.82.72 1.21 1.87.87 2.33.66.07-.52.28-.87.51-1.07-1.78-.2-3.64-.89-3.64-3.95 0-.87.31-1.59.82-2.15-.08-.2-.36-1.02.08-2.12 0 0 .67-.21 2.2.82.64-.18 1.32-.27 2-.27.68 0 1.36.09 2 .27 1.53-1.04 2.2-.82 2.2-.82.44 1.1.16 1.92.08 2.12.51.56.82 1.27.82 2.15 0 3.07-1.87 3.75-3.65 3.95.29.25.54.73.54 1.48 0 1.07-.01 1.93-.01 2.2 0 .21.15.46.55.38A8.013 8.013 0 0 0 16 8c0-4.42-3.58-8-8-8z"></path>
+          </svg>
+        </i>
+      </a>
+    </p>
+  </div>
+</div>
+
+<div class="w3-container w3-black w3-center w3-opacity w3-padding-64">
+  <h1 class="w3-margin w3-xlarge">Inspired by The Witness</h1>
+</div>
+
+<!-- footer -->
+<footer class="w3-container w3-padding-16 w3-center w3-opacity">
+ <p>Powered by <a href="https://www.w3schools.com/w3css/default.asp" target="_blank">w3.css</a></p>
+</footer>
+
+</body>
+</html>