my forest
lss links
+7
-3
+1
-1
trees/isa/isa-0001.tree
+1
-1
trees/isa/isa-0001.tree
···
1
1
\title{Interactive theorem proving}
2
2
\author{liamoc}
3
3
\taxon{Lecture Notes}
4
-
\p{These notes are the basis of my short course at the [ANU](anu) Logic Summer School 2025.}
4
+
\p{These notes are the basis of my short course at the [ANU](anu) [Logic Summer School 2025](loc-001W).}
5
5
\transclude{isa-0002}
6
6
\transclude{isa-001B}
7
7
\transclude{isa-002N}
+1
-1
trees/loc-002M.tree
+1
-1
trees/loc-002M.tree
···
4
4
\figure{
5
5
\<html:img>[width]{250px}[src]{\route-asset{assets/lss5.jpeg}}{}
6
6
}
7
-
\p{The first week of the [ANU](anu) Logic Summer School has concluded, including my introductory course on [[isa-0001]]. I think the course went well and students learnt a little of what makes theorem proving fun. Chelsea Edmonds will follow on from my course in week 2 with her own course on software verification. I hope I prepared the students well. We went on an excursion to the Tidbinbilla nature reserve (photos of which I have also previously shared on [[2025-W27]] and [[2025-W44]]).}
7
+
\p{The first week of the [ANU](anu) [Logic Summer School](loc-001W) has concluded, including my introductory course on [[isa-0001]]. I think the course went well and students learnt a little of what makes theorem proving fun. Chelsea Edmonds will follow on from my course in week 2 with her own course on software verification. I hope I prepared the students well. We went on an excursion to the Tidbinbilla nature reserve (photos of which I have also previously shared on [[2025-W27]] and [[2025-W44]]).}
8
8
\figure{
9
9
\<html:img>[width]{250px}[src]{\route-asset{assets/lss4.jpeg}}{}
10
10
\<html:img>[width]{250px}[src]{\route-asset{assets/lss3.jpeg}}{}
+4
trees/news.tree
+4
trees/news.tree
+1
-1
trees/weeknotes/2025-W49.tree
+1
-1
trees/weeknotes/2025-W49.tree
···
2
2
\title{Weeknotes 2025-W49}
3
3
\author{liamoc}
4
4
\date{2025-12-07}
5
-
\p{Much of this past week was spent organising for my Logic Summer School course or preparing for the Service of Lessons and Carols at Ainslie. Both went well I think! But I was so exhausted last night that these weeknotes are a day late.}
5
+
\p{Much of this past week was spent organising for my [Logic Summer School](loc-001W) course or preparing for the Service of Lessons and Carols at Ainslie. Both went well I think! But I was so exhausted last night that these weeknotes are a day late.}
6
6
\transclude{loc-002M}
7
7
\transclude{loc-002L}