Leanprover - Revision history

2A0B:F4C0:16C:16:0:0:0:1: blockquote quote from about page

2024-08-30T23:25:46Z

blockquote quote from about page

← Older revision		Revision as of 16:25, 30 August 2024
Line 1:		Line 1:
	Lean 4 Theorem Prover study session is for people who are studying and learning how to use the Lean theorem prover and dependently typed functional programming language.		Lean 4 Theorem Prover study session is for people who are studying and learning how to use the Lean theorem prover and dependently typed functional programming language.

			Quoting from https://lean-lang.org/about/:
			<blockquote>
	Lean is a functional programming language that makes it easy to write correct and maintainable code.		Lean is a functional programming language that makes it easy to write correct and maintainable code.

Line 24:		Line 24:

	For installing Lean 4, please see [https://lean-lang.org/download Download]. Information about the community of Lean users and the mathematical components library Mathlib can be found at the [https://leanprover-community.github.io/ Lean Community website].		For installing Lean 4, please see [https://lean-lang.org/download Download]. Information about the community of Lean users and the mathematical components library Mathlib can be found at the [https://leanprover-community.github.io/ Lean Community website].
			</blockquote>
	~~https://lean-lang.org/about/~~

	~~https://lean-lang.org~~/

	https://lean-lang.org/documentation/		https://lean-lang.org/documentation/


	'''''Watch this talk about Lean by Terry Tao!''''' https://www.youtube.com/watch?v=AayZuuDDKP0		'''''Watch this talk about Lean by Terry Tao!''''' https://www.youtube.com/watch?v=AayZuuDDKP0


	As a study group we are interested in these activities:		As a study group we are interested in these activities:

David415: added another book recommendation to the lean theorem prover page

2024-08-28T03:38:13Z

added another book recommendation to the lean theorem prover page

← Older revision		Revision as of 20:38, 27 August 2024
Line 47:		Line 47:
	* The Mechanics of Proof https://hrmacbeth.github.io/math2001/		* The Mechanics of Proof https://hrmacbeth.github.io/math2001/
	* functional programming in lean https://lean-lang.org/functional_programming_in_lean/		* functional programming in lean https://lean-lang.org/functional_programming_in_lean/
			* How to Prove It: A Structured Approach by Daniel J. Velleman (third edition)
	* Category Theory For Programmers https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/		* Category Theory For Programmers https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/

David415: minor update to lean theorem prover page

2024-08-28T03:19:01Z

minor update to lean theorem prover page

← Older revision		Revision as of 20:19, 27 August 2024
Line 2:		Line 2:


	Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover. Lean programming primarily involves defining types and functions. This allows your focus to remain on the problem domain and manipulating its data, rather than the details of programming. Lean has numerous features, including:
			Lean is a functional programming language that makes it easy to write correct and maintainable code.

			You can also use Lean as an interactive theorem prover. Lean programming primarily involves defining types and functions.

			This allows your focus to remain on the problem domain and manipulating its data, rather than the details of programming. Lean has numerous features, including:

	* Type inference		* Type inference
Line 20:		Line 25:
	For installing Lean 4, please see [https://lean-lang.org/download Download]. Information about the community of Lean users and the mathematical components library Mathlib can be found at the [https://leanprover-community.github.io/ Lean Community website].		For installing Lean 4, please see [https://lean-lang.org/download Download]. Information about the community of Lean users and the mathematical components library Mathlib can be found at the [https://leanprover-community.github.io/ Lean Community website].

	~~The Lean FRO nonprofit was launched in August of 2023. Its mission is to tackle the challenges of scalability, usability, and proof automation in the Lean theorem prover~~.		https://lean-lang.org/about/

	https://lean-lang.org/		https://lean-lang.org/

David415: update lean theorem prover study page

2024-08-28T03:16:59Z

update lean theorem prover study page

@@ Line 1: / Line 1: @@
 Lean 4 Theorem Prover study session is for people who are studying and learning how to use the Lean theorem prover and dependently typed functional programming language.
 https://lean-lang.org/
@@ Line 6: / Line 27: @@
-We are interested in:
+'''''Watch this talk about Lean by Terry Tao!''''' https://www.youtube.com/watch?v=AayZuuDDKP0
 * pair programming in Lean or Lean code review sessions
@@ Line 18: / Line 42: @@
 * The Mechanics of Proof https://hrmacbeth.github.io/math2001/
 * functional programming in lean https://lean-lang.org/functional_programming_in_lean/
-* Category Theory For Programmers
+* Category Theory For Programmers https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/
-Questions? We hang out on the Lean community Zulip chat and you can find us here:
+In the San Francisco geographical section:
 https://leanprover.zulipchat.com/#narrow/stream/224796-Geographic-locality/topic/San.20Francisco.2C.20CA.2C.20USA

David415: add a humble little page for the Lean theorem prover study meet

2024-08-28T02:59:19Z

add a humble little page for the Lean theorem prover study meet

New page

Lean 4 Theorem Prover study session is for people who are studying and learning how to use the Lean theorem prover and dependently typed functional programming language.

https://lean-lang.org/

https://lean-lang.org/documentation/

We are interested in:

* pair programming in Lean or Lean code review sessions

* discussing Lean topics such as program verification, functional programming, category theory, type theory, monads, monoids etc.
* book discussion / review exercises

Which books are we interested in?

* The Mechanics of Proof https://hrmacbeth.github.io/math2001/
* functional programming in lean https://lean-lang.org/functional_programming_in_lean/
* Category Theory For Programmers

Questions? We hang out on the Lean community Zulip chat and you can find us here:

https://leanprover.zulipchat.com/#narrow/stream/224796-Geographic-locality/topic/San.20Francisco.2C.20CA.2C.20USA